proposition: Lemma cpn7_uclo uclo (MON: monotone7 uclo) (WCOM: forall r, uclo (gf r) <7= gf (gupaco7 gf (uclo \8/ cpn7) r)): uclo <8= gupaco7 gf cpn7.
proof: Proof. intros. apply gpaco7_clo. exists (gupaco7 gf (uclo \8/ cpn7)). - apply wcompat7_compat. apply gf_mon. econstructor. + apply monotone7_union. apply MON. apply cpn7_mon. + intros. destruct PR0. * apply WCOM, H. * apply compat7_compat with (gf:=gf) in H; [| apply cpn7_compat]. eapply gf_mon. apply H. intros. apply gpaco7_clo. right. apply PR0. - apply gpaco7_clo. left. apply PR. Qed.
imports: Program.Basics Paco(paco7 pacotac)