proposition: Lemma cpn14_uclo uclo (MON: monotone14 uclo) (WCOM: forall r, uclo (gf r) <14= gf (gupaco14 gf (uclo \15/ cpn14) r)): uclo <15= gupaco14 gf cpn14.
proof: Proof. intros. apply gpaco14_clo. exists (gupaco14 gf (uclo \15/ cpn14)). - apply wcompat14_compat. apply gf_mon. econstructor. + apply monotone14_union. apply MON. apply cpn14_mon. + intros. destruct PR0. * apply WCOM, H. * apply compat14_compat with (gf:=gf) in H; [| apply cpn14_compat]. eapply gf_mon. apply H. intros. apply gpaco14_clo. right. apply PR0. - apply gpaco14_clo. left. apply PR. Qed.
imports: Program.Basics Paco(paco14 pacotac)