remove the empty class and the wild card object; implement bracketed binders; fix inference rule 'cast'

Now cast is implemented like this:

    cast : (T:texp) ⟶ (U:texp) ⟶ (o:oexp) ⟶ (x:Singleton(o : oexp)) × istype T ⟶ istype U ⟶ tequal T U ⟶ hastype o T ⟶ hastype x U

and coded like this:

    Axiom 3.4.13 cast { ⊢ T U Type } [ T ≡ U ] { ⊢ o : T } ⊢ o : U.

so now it is possible to write cast[T,U,o,CAR] to extract the specified TS expression, which
is just o, of course, so one knows it, but we want all inferences rules to have their
expression parts expressible as terms.