proposition: Theorem paco10_unfold: forall (MON: monotone10 gf) r, paco10 gf r <10= gf (upaco10 gf r).
proof: Proof. intro. eapply _paco10_unfold; apply monotone10_eq; assumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)