getting started on full type safety proof.

copied most of ../dev/dot.elf and tweaked it. var case goes through.