proposition: Lemma gpaco7_init clo (WCMP: wcompatible7 gf clo): gpaco7 gf clo bot7 bot7 <7= paco7 gf bot7.
proof: Proof. intros. eapply gpaco7_compat_init. - apply wcompat7_compat, WCMP. apply gf_mon. - eapply gpaco7_mon_bot. apply PR. apply gf_mon. intros; apply PR0. intros. apply gpaco7_clo, PR0. Qed.
imports: Program.Basics Paco(paco7 pacotac)