proposition: Lemma cpn8_uclo uclo (MON: monotone8 uclo) (WCOM: forall r, uclo (gf r) <8= gf (gupaco8 gf (uclo \9/ cpn8) r)): uclo <9= gupaco8 gf cpn8.
proof: Proof. intros. apply gpaco8_clo. exists (gupaco8 gf (uclo \9/ cpn8)). - apply wcompat8_compat. apply gf_mon. econstructor. + apply monotone8_union. apply MON. apply cpn8_mon. + intros. destruct PR0. * apply WCOM, H. * apply compat8_compat with (gf:=gf) in H; [| apply cpn8_compat]. eapply gf_mon. apply H. intros. apply gpaco8_clo. right. apply PR0. - apply gpaco8_clo. left. apply PR. Qed.
imports: Program.Basics Paco(paco8 pacotac)