proposition: Lemma cpn3_uclo uclo (MON: monotone3 uclo) (WCOM: forall r, uclo (gf r) <3= gf (gupaco3 gf (uclo \4/ cpn3) r)): uclo <4= gupaco3 gf cpn3.
proof: Proof. intros. apply gpaco3_clo. exists (gupaco3 gf (uclo \4/ cpn3)). - apply wcompat3_compat. apply gf_mon. econstructor. + apply monotone3_union. apply MON. apply cpn3_mon. + intros. destruct PR0. * apply WCOM, H. * apply compat3_compat with (gf:=gf) in H; [| apply cpn3_compat]. eapply gf_mon. apply H. intros. apply gpaco3_clo. right. apply PR0. - apply gpaco3_clo. left. apply PR. Qed.
imports: Program.Basics Paco(paco3 pacotac)