proposition: Theorem paco8_unfold: forall (MON: monotone8 gf) r, paco8 gf r <8= gf (upaco8 gf r).
proof: Proof. intro. eapply _paco8_unfold; apply monotone8_eq; assumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)