Explicit instantiation is not the only way to prove the three conjectures about union in set1.lp. Here's another technique:

The prove command directs LP to begin an attempt to prove the conjecture by contradiction. LP does this by adding the negation,prove x \union {} = x by contradiction critical-pairs *Hyp with extensionality qed

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

The extensionality axiom rewrites this formula to\A e (e \in (xc \union {}) <=> e \in xc) => xc \union {} = xc

Hence these two results must be equivalent:\A e (e \in (xc \union {}) <=> e \in xc) => false

As in our first proof of the conjecture, this formula rewrites to\A e (e \in (xc \union {}) <=> e \in xc) => false <=> true

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