proposition: Lemma gpaco8_init clo (WCMP: wcompatible8 gf clo): gpaco8 gf clo bot8 bot8 <8= paco8 gf bot8.
proof: Proof. intros. eapply gpaco8_compat_init. - apply wcompat8_compat, WCMP. apply gf_mon. - eapply gpaco8_mon_bot. apply PR. apply gf_mon. intros; apply PR0. intros. apply gpaco8_clo, PR0. Qed.
imports: Program.Basics Paco(paco8 pacotac)