proposition: Lemma cpn6_uclo uclo (MON: monotone6 uclo) (WCOM: forall r, uclo (gf r) <6= gf (gupaco6 gf (uclo \7/ cpn6) r)): uclo <7= gupaco6 gf cpn6.
proof: Proof. intros. apply gpaco6_clo. exists (gupaco6 gf (uclo \7/ cpn6)). - apply wcompat6_compat. apply gf_mon. econstructor. + apply monotone6_union. apply MON. apply cpn6_mon. + intros. destruct PR0. * apply WCOM, H. * apply compat6_compat with (gf:=gf) in H; [| apply cpn6_compat]. eapply gf_mon. apply H. intros. apply gpaco6_clo. right. apply PR0. - apply gpaco6_clo. left. apply PR. Qed.
imports: Program.Basics Paco(paco6 pacotac)