proposition: Theorem paco2_unfold: forall (MON: monotone2 gf) r, paco2 gf r <2= gf (upaco2 gf r).
proof: Proof. intro. eapply _paco2_unfold; apply monotone2_eq; assumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)