proposition: Lemma cpn9_uclo uclo (MON: monotone9 uclo) (WCOM: forall r, uclo (gf r) <9= gf (gupaco9 gf (uclo \10/ cpn9) r)): uclo <10= gupaco9 gf cpn9.
proof: Proof. intros. apply gpaco9_clo. exists (gupaco9 gf (uclo \10/ cpn9)). - apply wcompat9_compat. apply gf_mon. econstructor. + apply monotone9_union. apply MON. apply cpn9_mon. + intros. destruct PR0. * apply WCOM, H. * apply compat9_compat with (gf:=gf) in H; [| apply cpn9_compat]. eapply gf_mon. apply H. intros. apply gpaco9_clo. right. apply PR0. - apply gpaco9_clo. left. apply PR. Qed.
imports: Program.Basics Paco(paco9 pacotac)