proposition: Lemma gpaco12_init clo (WCMP: wcompatible12 gf clo): gpaco12 gf clo bot12 bot12 <12= paco12 gf bot12.
proof: Proof. intros. eapply gpaco12_compat_init. - apply wcompat12_compat, WCMP. apply gf_mon. - eapply gpaco12_mon_bot. apply PR. apply gf_mon. intros; apply PR0. intros. apply gpaco12_clo, PR0. Qed.
imports: Program.Basics Paco(paco12 pacotac)