more equational proofs
	modified:   EMAdj2.agda