proposition: Theorem paco3_unfold: forall (MON: monotone3 gf) r, paco3 gf r <3= gf (upaco3 gf r).
proof: Proof. intro. eapply _paco3_unfold; apply monotone3_eq; assumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)