proposition: Theorem paco12_unfold: forall (MON: monotone12 gf) r, paco12 gf r <12= gf (upaco12 gf r).
proof: Proof. intro. eapply _paco12_unfold; apply monotone12_eq; assumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)