use α×num rather than α list for the example model of set theory

this makes clearer what's going on: we want to use num, but need a type
variable for infinite sets.
move dbterm stuff into sholSyntaxExtra

from sholSemantics, where it was tangential
switch from α×num to α+num

suggestion from Rob.
this is even more economical as an example model of the set theory.
prove all term_ok terms and stateless sequents are well-typed

hoping this is enough syntactic information to allow proves_IMP to be
proved without appeal to the soundness proof.
remove is_model hypothesis from proves_IMP
removing is_model from hol_verification, one cheat
prove cheat for sequent_has_type_bool
encoding of tuples and n-ary cartesian products in set theory

in case they are useful later...
use type lem instead of [ -x lem ] in Holmakefiles

the latter seems not to work, since I guess it doesn't search in the
$PATH, whereas type is supposed to treat the argument as if it were a
command you wrote at the shell.
Merge remote-tracking branch 'origin/master' into cenv_close

Conflicts:
	semantics/Holmakefile
Move the type soundness invariant into a Lem file
More de-crufting