v should be a variable. Generalizes occurrences
of t as subterms of the concl to variable v. Adds new hypotheses
declaring v to be of type T and stating that .
ApFunToHypEquands (x:var) (:term) (:term) (i:int)
If hypothesis i is of form , then this tactic
applies the function to the terms a and b to give
a new hypothesis in the subgoal labelled main of form
. Also creates a couple of aux subgoals. See file
inclusion-tactics.ml for details.