proposition: Theorem paco7_unfold: forall (MON: monotone7 gf) r, paco7 gf r <7= gf (upaco7 gf r).
proof: Proof. intro. eapply _paco7_unfold; apply monotone7_eq; assumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)