Basically reduce the conservativity proof to a few cheated lemmas

The remaining problem is that the straightforward proof outline of just
structurally replacing constants with their definitions in a proof tree
doesn't quite work. The problem is that the TERM_UNION construction
removes duplicate assumptions (up to alpha equivalence), and removing
definitions might introduce duplicates.

A similar same thing happens in the deduct_antisym rule.

Suppose we define a constant c = \x. x > 0

Then we can prove

x = y, c y |- c x

and

x = y, c x |- y > 0

and by deduct_antisym

x = y, c y |- c x = y > 0

Now if we replace c with it's definition in the proof we try to do the
following, which is not a valid application of DEDUCT_ANTISYM

x = y, y > 0 |- x > 0
x = y, x > 0 |- y > 0
---------------------------- DEDUCT_ANTISYM
x = y, y > 0 |- x > 0 = y > 0

Instead we need

x = y, y > 0 |- x > 0
x = y, x > 0 |- y > 0
---------------------------- DEDUCT_ANTISYM
x = y |- x > 0 = y > 0
---------------------------- Weakening
x = y, y > 0 |- x > 0 = y > 0