proposition: Lemma gpaco10_init clo (WCMP: wcompatible10 gf clo): gpaco10 gf clo bot10 bot10 <10= paco10 gf bot10.
proof: Proof. intros. eapply gpaco10_compat_init. - apply wcompat10_compat, WCMP. apply gf_mon. - eapply gpaco10_mon_bot. apply PR. apply gf_mon. intros; apply PR0. intros. apply gpaco10_clo, PR0. Qed.
imports: Program.Basics Paco(paco10 pacotac)