proving typeof decider
Car proven; proving Cdr
Cdr proved; proving general App
App proven; proving Let
Let proved; proving Cons
TypeOf_dec finished; Var axiom remains