equational proofs for remfunctors2
	modified:   REMFunctors2.agda