proposition: Lemma cpn4_uclo uclo (MON: monotone4 uclo) (WCOM: forall r, uclo (gf r) <4= gf (gupaco4 gf (uclo \5/ cpn4) r)): uclo <5= gupaco4 gf cpn4.
proof: Proof. intros. apply gpaco4_clo. exists (gupaco4 gf (uclo \5/ cpn4)). - apply wcompat4_compat. apply gf_mon. econstructor. + apply monotone4_union. apply MON. apply cpn4_mon. + intros. destruct PR0. * apply WCOM, H. * apply compat4_compat with (gf:=gf) in H; [| apply cpn4_compat]. eapply gf_mon. apply H. intros. apply gpaco4_clo. right. apply PR0. - apply gpaco4_clo. left. apply PR. Qed.
imports: Program.Basics Paco(paco4 pacotac)