proposition: Lemma monotone1_eq (gf: rel1 T0 -> rel1 T0) : monotone1 gf <-> _monotone1 gf.
proof: Proof. unfold monotone1, _monotone1, le1. split; intros; eapply H; eassumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)