proposition: Theorem paco4_unfold: forall (MON: monotone4 gf) r, paco4 gf r <4= gf (upaco4 gf r).
proof: Proof. intro. eapply _paco4_unfold; apply monotone4_eq; assumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)