proposition: Lemma gpaco11_init clo (WCMP: wcompatible11 gf clo): gpaco11 gf clo bot11 bot11 <11= paco11 gf bot11.
proof: Proof. intros. eapply gpaco11_compat_init. - apply wcompat11_compat, WCMP. apply gf_mon. - eapply gpaco11_mon_bot. apply PR. apply gf_mon. intros; apply PR0. intros. apply gpaco11_clo, PR0. Qed.
imports: Program.Basics Paco(paco11 pacotac)