proposition: Theorem paco6_unfold: forall (MON: monotone6 gf) r, paco6 gf r <6= gf (upaco6 gf r).
proof: Proof. intro. eapply _paco6_unfold; apply monotone6_eq; assumption. Qed.
imports: Program.Basics Paco(paconotation_internal paco_internal pacotac_internal)