abandon de Bruijn syntax, prove VSUBST_simple_subst

the theorem says that VSUBST behaves the same as a simple subst
(non-capture-avoiding) under certain conditions (i.e. bound variable
names are all fresh enough).

the plan is to prove a similar theorem for INST (with a simple inst) and
then show it's always possible to create an alpha-equivalent term
satisfying the conditions.
prove INST_simple_inst
prove existence of alpha-convertible term with fresh bound names

all distinct bound names fresh for an arbitrary finite set.
this should enable use of simple-inst and simple-subst whenever working
up to alpha-equivalence.
define the semantics with simple_inst, and prove it 11
prove the semantics of ACONV terms are the same

proof basically copied from before.
prove aconv sym and trans and respected by tvars
prove simple_inst_aconv and semantics_closes
prove semantics_typeset
prove up to has_meaning_Comb

has_meaning seems to require an extra assumption that the types of all
free variables in the term have a meaning... since we restrict attention
to valuations that close over the term, this prevents a term with bad
types having a meaning vacuously...
make closes take domains rather than whole maps
prove has_meaning_Abs
prove semantics_has_meaning and has_meaning_aconv
prove equation_has_meaning, and prove ASSUME and REFL correct
prove binary_inference_rule and correctness of rules up to BETA
delete some commented out stuff, fix proof by reordering defs
prove ABS_correct
prove DEDUCT_ANTISYM_correct
start trying to prove semantics_simple_subst
prove semantics_simple_subst
start trying to prove RACONV_VSUBST

getting the statement right is going to be very difficult