proposition: Theorem paco5_unfold: forall (MON: monotone5 gf) r, paco5 gf r <5= gf (upaco5 gf r).
proof: Proof. intro. eapply _paco5_unfold; apply monotone5_eq; assumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)