updated proofs
	modified:   WellTypedTerms3.agda