updated and simplified proofs
	modified:   WellTypedTermsModel3.agda