# LP, the Larch Prover -- Proofs of logical equivalence

The command `prove t1 <=> t2 by <=>` directs LP to prove the conjecture by
proving two implications, `t1 => t2` and `t2 => t1`. LP substitutes new
constants for the free variables in both `t1` and `t2`
to obtain terms `t1'` and `t2'`, and it creates two subgoals: the first
involves proving `t2'` using `t1'` as an additional hypothesis, the
second proving `t1'` using `t2'` as an additional hypothesis. The names
of the hypotheses have the form <simpleId>`ImpliesHyp.`<number>, where
<simpleId> is the current value of the name-prefix setting.
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 a formula of the form `t1 <=> t2` or of the
form `t1 = t2` when `t1` and `t2` are boolean-valued terms.