checkpoint before adding encoding of let rec
top-level recursive functions encoded to Z3; some simple extrinsic inductive proofs about total functions work; also added b2t coercions
 note about b2t