equationalising
	modified:   EMAdj2.agda