directs LP to prove the subgoal t2' using the hypothesis t1', where t1' and t2' are obtained as in a proof by cases, that is, by substituting new constants for the free variables of t1 in both t1 and t2. The name of the hypothesis has the form <simpleId>ImpliesHyp.<number>, where <simpleId> is the current value of the name-prefix setting.prove t1 => t2 by =>
For example, given the axioms a => b and b => c, the command prove a => c by => orients the hypothesis a into a rewrite rule a -> true and attempts to prove c as a subgoal. The proof succeeds automatically: LP orients the hypothesis into a rewrite rule a -> true, uses it to normalize the first axiom to b, orients the result into a rewrite rule b -> true, and uses it to normalize the second axiom to c, which establishes the subgoal.
The command resume by => directs LP to resume the proof of the current conjecture using this method. It is applicable only when the current conjecture has been reduced to an implication.
Users should beware of using the => proof method prematurely, because it causes LP to replace all free variables in the conjecture by constants, which makes it impossible to continue the proof by induction on one of those variables.