work on substitution_preserves_typing