equational proof for the rest of well scoped terms
	modified:   WellScopedTerms.agda