proposition: Lemma gpaco14_init clo (WCMP: wcompatible14 gf clo): gpaco14 gf clo bot14 bot14 <14= paco14 gf bot14.
proof: Proof. intros. eapply gpaco14_compat_init. - apply wcompat14_compat, WCMP. apply gf_mon. - eapply gpaco14_mon_bot. apply PR. apply gf_mon. intros; apply PR0. intros. apply gpaco14_clo, PR0. Qed.
imports: Program.Basics Paco(paco14 pacotac)