proposition: Theorem paco1_unfold: forall (MON: monotone1 gf) r, paco1 gf r <1= gf (upaco1 gf r).
proof: Proof. intro. eapply _paco1_unfold; apply monotone1_eq; assumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)