Trying to existentially quantify type substitutions

Rather than computing a substitution for matching.
Changed list pretty printer (for CakeML lists)
Fix up list pretty printing and extend up to modLang
Add missing alist defs to inference compset
Removing cheats
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
add special pretty-printing for Dlet (Pvar x) (Fun y z)

make it look like a fun declaration rather than a val = fn.
make build sequence match explorer dependencies better
An incomplete development of weight balanced trees

Eventually this will get completed and moved into HOL4 itself. Currently
supports insert, delete, union, submap, map, to_list, and comparison of
trees.
Remove spurious TODO
Add pair_cmp for building comparisons
Add comparison for strings and numbers
More congruence rules

But the pair_cmp_cong one doesn't seem to work...
Added a simple fromList function
Merge remote-tracking branch 'origin/master' into char
get bootstrap building