proposition: Lemma cpn12_uclo uclo (MON: monotone12 uclo) (WCOM: forall r, uclo (gf r) <12= gf (gupaco12 gf (uclo \13/ cpn12) r)): uclo <13= gupaco12 gf cpn12.
proof: Proof. intros. apply gpaco12_clo. exists (gupaco12 gf (uclo \13/ cpn12)). - apply wcompat12_compat. apply gf_mon. econstructor. + apply monotone12_union. apply MON. apply cpn12_mon. + intros. destruct PR0. * apply WCOM, H. * apply compat12_compat with (gf:=gf) in H; [| apply cpn12_compat]. eapply gf_mon. apply H. intros. apply gpaco12_clo. right. apply PR0. - apply gpaco12_clo. left. apply PR. Qed.
imports: Program.Basics Paco(paco12 pacotac)