LP, the Larch Prover -- Sample proofs: alternative proofs of theorems about union

Explicit instantiation is not the only way to prove the three conjectures about union in set1.lp. Here's another technique: 
prove x \union {} = x by contradiction
  critical-pairs *Hyp with extensionality
qed
The prove command directs LP to begin an attempt to prove the conjecture by contradiction. LP does this by adding the negation, ~(xc \union {} = xc), of the conjecture as a hypothesis to its logical system. It replaces the variable x in the conjecture by the constant xc, because the negation of a conjecture about all sets x is a statement about some particular set xc. LP also orients this new hypothesis into a rewrite rule, xc \union {} = xc -> false.

The critical-pairs command directs LP to use the rewrite rule obtained from this new hypothesis, whose name setTheoremsContraHyp.1 matches the pattern *Hyp, together with that obtained from the fact whose name matches extensionality, to enlarge its set of rewrite rules. LP does this by finding a term that can be rewritten in two different ways by the two rewrite rules and then asserting that these two terms must be equal. LP finds such a term by unifying the left side of one rewrite rule with a subterm of the left side of the other. Here, LP unifies the left side of the hypothesized rewrite rule with a subterm of the extensionality principle (by mapping x to xc \union {} and y to xc) to obtain the formula 

\A e (e \in (xc \union {}) <=> e \in xc) => xc \union {} = xc
The extensionality axiom rewrites this formula to true, whereas the hypothesized rewrite rule rewrites it to 
\A e (e \in (xc \union {}) <=> e \in xc) => false
Hence these two results must be equivalent: 
\A e (e \in (xc \union {}) <=> e \in xc) => false <=> true
As in our first proof of the conjecture, this formula rewrites to true => false <=> true, which rewrites to false using LP's hardwired axioms. This inconsistency finishes the proof by contradiction.

The file set1.lp uses this technique to prove the second and third theorems about union.