proposition: Lemma cpn5_uclo uclo (MON: monotone5 uclo) (WCOM: forall r, uclo (gf r) <5= gf (gupaco5 gf (uclo \6/ cpn5) r)): uclo <6= gupaco5 gf cpn5.
proof: Proof. intros. apply gpaco5_clo. exists (gupaco5 gf (uclo \6/ cpn5)). - apply wcompat5_compat. apply gf_mon. econstructor. + apply monotone5_union. apply MON. apply cpn5_mon. + intros. destruct PR0. * apply WCOM, H. * apply compat5_compat with (gf:=gf) in H; [| apply cpn5_compat]. eapply gf_mon. apply H. intros. apply gpaco5_clo. right. apply PR0. - apply gpaco5_clo. left. apply PR. Qed.
imports: Program.Basics Paco(paco5 pacotac)