Proofs of implications can be carried out using a simplified form of a proof by cases. The command

directs LP to prove the subgoalprove 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.