proposition: Theorem paco14_unfold: forall (MON: monotone14 gf) r, paco14 gf r <14= gf (upaco14 gf r).
proof: Proof. intro. eapply _paco14_unfold; apply monotone14_eq; assumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)