proposition: Lemma cpn2_uclo uclo (MON: monotone2 uclo) (WCOM: forall r, uclo (gf r) <2= gf (gupaco2 gf (uclo \3/ cpn2) r)): uclo <3= gupaco2 gf cpn2.
proof: Proof. intros. apply gpaco2_clo. exists (gupaco2 gf (uclo \3/ cpn2)). - apply wcompat2_compat. apply gf_mon. econstructor. + apply monotone2_union. apply MON. apply cpn2_mon. + intros. destruct PR0. * apply WCOM, H. * apply compat2_compat with (gf:=gf) in H; [| apply cpn2_compat]. eapply gf_mon. apply H. intros. apply gpaco2_clo. right. apply PR0. - apply gpaco2_clo. left. apply PR. Qed.
imports: Program.Basics Paco(paco2 pacotac)