equation proofs in TFun
	modified:   RMonads2.agda