proposition: Lemma monotone0_eq (gf: rel0 -> rel0) : monotone0 gf <-> _monotone0 gf.
proof: Proof. unfold monotone0, _monotone0, le0. split; intros; eapply H; eassumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)