Starting proof inductions, have a few but only in TypeSafetyProof.v