cleaned up substitution_preserves_typing proof, some organizational things