equational proofs in Kleisli
	modified:   Kleisli2.agda