proposition: Lemma gpaco6_init clo (WCMP: wcompatible6 gf clo): gpaco6 gf clo bot6 bot6 <6= paco6 gf bot6.
proof: Proof. intros. eapply gpaco6_compat_init. - apply wcompat6_compat, WCMP. apply gf_mon. - eapply gpaco6_mon_bot. apply PR. apply gf_mon. intros; apply PR0. intros. apply gpaco6_clo, PR0. Qed.
imports: Program.Basics Paco(paco6 pacotac)