proposition: Theorem _paco_unfold: forall (MON: _monotone gf) r, paco gf r <1== gf (upaco gf r).
proof: Proof. unfold le1. intro. eapply paco_unfold; apply monotone_eq; eauto. Qed.
imports: Paco(pacotac_internal paconotation_internal)