proposition: Lemma cpn1_uclo uclo (MON: monotone1 uclo) (WCOM: forall r, uclo (gf r) <1= gf (gupaco1 gf (uclo \2/ cpn1) r)): uclo <2= gupaco1 gf cpn1.
proof: Proof. intros. apply gpaco1_clo. exists (gupaco1 gf (uclo \2/ cpn1)). - apply wcompat1_compat. apply gf_mon. econstructor. + apply monotone1_union. apply MON. apply cpn1_mon. + intros. destruct PR0. * apply WCOM, H. * apply compat1_compat with (gf:=gf) in H; [| apply cpn1_compat]. eapply gf_mon. apply H. intros. apply gpaco1_clo. right. apply PR0. - apply gpaco1_clo. left. apply PR. Qed.
imports: Program.Basics Paco(paco1 pacotac)