proposition: Lemma cpn11_uclo uclo (MON: monotone11 uclo) (WCOM: forall r, uclo (gf r) <11= gf (gupaco11 gf (uclo \12/ cpn11) r)): uclo <12= gupaco11 gf cpn11.
proof: Proof. intros. apply gpaco11_clo. exists (gupaco11 gf (uclo \12/ cpn11)). - apply wcompat11_compat. apply gf_mon. econstructor. + apply monotone11_union. apply MON. apply cpn11_mon. + intros. destruct PR0. * apply WCOM, H. * apply compat11_compat with (gf:=gf) in H; [| apply cpn11_compat]. eapply gf_mon. apply H. intros. apply gpaco11_clo. right. apply PR0. - apply gpaco11_clo. left. apply PR. Qed.
imports: Program.Basics Paco(paco11 pacotac)