proposition: Lemma gpaco9_init clo (WCMP: wcompatible9 gf clo): gpaco9 gf clo bot9 bot9 <9= paco9 gf bot9.
proof: Proof. intros. eapply gpaco9_compat_init. - apply wcompat9_compat, WCMP. apply gf_mon. - eapply gpaco9_mon_bot. apply PR. apply gf_mon. intros; apply PR0. intros. apply gpaco9_clo, PR0. Qed.
imports: Program.Basics Paco(paco9 pacotac)