proposition: Lemma cpn0_uclo uclo (MON: monotone0 uclo) (WCOM: forall r, uclo (gf r) <0= gf (gupaco0 gf (uclo \1/ cpn0) r)): uclo <1= gupaco0 gf cpn0.
proof: Proof. intros. apply gpaco0_clo. exists (gupaco0 gf (uclo \1/ cpn0)). - apply wcompat0_compat. apply gf_mon. econstructor. + apply monotone0_union. apply MON. apply cpn0_mon. + intros. destruct PR0. * apply WCOM, H. * apply compat0_compat with (gf:=gf) in H; [| apply cpn0_compat]. eapply gf_mon. apply H. intros. apply gpaco0_clo. right. apply PR0. - apply gpaco0_clo. left. apply PR. Qed.
imports: Program.Basics Paco(paco0 pacotac)