proposition: Lemma monotone5_eq (gf: rel5 T0 T1 T2 T3 T4 -> rel5 T0 T1 T2 T3 T4) : monotone5 gf <-> _monotone5 gf.
proof: Proof. unfold monotone5, _monotone5, le5. split; intros; eapply H; eassumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)