proposition: Lemma monotone3_eq (gf: rel3 T0 T1 T2 -> rel3 T0 T1 T2) : monotone3 gf <-> _monotone3 gf.
proof: Proof. unfold monotone3, _monotone3, le3. split; intros; eapply H; eassumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)