proposition: Theorem paco0_unfold: forall (MON: monotone0 gf) r, paco0 gf r <0= gf (upaco0 gf r).
proof: Proof. intro. eapply _paco0_unfold; apply monotone0_eq; assumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)