proposition: Lemma cpn13_uclo uclo (MON: monotone13 uclo) (WCOM: forall r, uclo (gf r) <13= gf (gupaco13 gf (uclo \14/ cpn13) r)): uclo <14= gupaco13 gf cpn13.
proof: Proof. intros. apply gpaco13_clo. exists (gupaco13 gf (uclo \14/ cpn13)). - apply wcompat13_compat. apply gf_mon. econstructor. + apply monotone13_union. apply MON. apply cpn13_mon. + intros. destruct PR0. * apply WCOM, H. * apply compat13_compat with (gf:=gf) in H; [| apply cpn13_compat]. eapply gf_mon. apply H. intros. apply gpaco13_clo. right. apply PR0. - apply gpaco13_clo. left. apply PR. Qed.
imports: Program.Basics Paco(paco13 pacotac)