proposition: Theorem paco_unfold: forall (MON: monotone gf) r, paco gf r <1= gf (upaco gf r).
proof: Proof. unfold monotone; intros; apply paco_observe in PR; destruct PR as []; eauto. Qed.
imports: Paco(pacotac_internal paconotation_internal)