Attempt to prove monotonicity hypotheses of theorem automatically.
DESCRIPTION
Given a theorem A |- t, the rule prove_monotonicity_hyps attempts to prove
and remove all hypotheses that are not equations, by breaking them down and
repeatedly using MONO_TAC. Any that are equations or are not automatically
provable will be left as they are.
FAILURE CONDITIONS
Never fails but may have no effect.
COMMENTS
Normally, this kind of reasoning is automated by the inductive definitions
package, so explicit use of this tactic is rare.