proposition: Theorem paco9_unfold: forall (MON: monotone9 gf) r, paco9 gf r <9= gf (upaco9 gf r).
proof: Proof. intro. eapply _paco9_unfold; apply monotone9_eq; assumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)