equation proofs for RKleisli2
	modified:   Everything.agda
	modified:   RKleisli2.agda