proposition: Theorem paco11_unfold: forall (MON: monotone11 gf) r, paco11 gf r <11= gf (upaco11 gf r).
proof: Proof. intro. eapply _paco11_unfold; apply monotone11_eq; assumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)