proposition: Lemma cpn10_uclo uclo (MON: monotone10 uclo) (WCOM: forall r, uclo (gf r) <10= gf (gupaco10 gf (uclo \11/ cpn10) r)): uclo <11= gupaco10 gf cpn10.
proof: Proof. intros. apply gpaco10_clo. exists (gupaco10 gf (uclo \11/ cpn10)). - apply wcompat10_compat. apply gf_mon. econstructor. + apply monotone10_union. apply MON. apply cpn10_mon. + intros. destruct PR0. * apply WCOM, H. * apply compat10_compat with (gf:=gf) in H; [| apply cpn10_compat]. eapply gf_mon. apply H. intros. apply gpaco10_clo. right. apply PR0. - apply gpaco10_clo. left. apply PR. Qed.
imports: Program.Basics Paco(paco10 pacotac)