Make problem simplification eliminate by substitution

[GoogleCodeExporter]

When defining functions by induction over indexed datatypes, the method 
hypotheses often contain equations that we need to manually substitute out. 
Problem simplification should perform an occur check, then eliminate by 
substitutivity of equality. If the occur check fails, it could perhaps observe 
a cycle and derive a contradiction from the hypothesis.

Original issue reported on code.google.com by adamgundry on 11 Jun 2010 at 8:06

[GoogleCodeExporter]

Done, at least in principle. Performance is barely adequate and some work needs 
to be done on figuring out why. More occur check magic could happen.

Original comment by adamgundry on 3 Aug 2010 at 1:39

• Changed state: Fixed