updated subren proof
	modified:   WellTypedTerms3.agda