proposition: Theorem paco13_unfold: forall (MON: monotone13 gf) r, paco13 gf r <13= gf (upaco13 gf r).
proof: Proof. intro. eapply _paco13_unfold; apply monotone13_eq; assumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)