* end of the proof of subject reduction