changed proofs in rel. EM + knock on effects
	modified:   EM2.agda
	modified:   REM2.agda
	modified:   REMAdj2.agda
	modified:   REMFunctors2.agda
	modified:   TermAdj2Hom.agda
	modified:   TermAdj2Uniq.agda
	modified:   TermRAdj2.agda
	modified:   TermRAdj2Hom.agda