Pat elaboration and decs done
VC fromTypeCheck done
VC generation code complete
substitution and instantiation fns in speclang
Verification Condition generation complete