proposition: Lemma gpaco2_init clo (WCMP: wcompatible2 gf clo): gpaco2 gf clo bot2 bot2 <2= paco2 gf bot2.
proof: Proof. intros. eapply gpaco2_compat_init. - apply wcompat2_compat, WCMP. apply gf_mon. - eapply gpaco2_mon_bot. apply PR. apply gf_mon. intros; apply PR0. intros. apply gpaco2_clo, PR0. Qed.
imports: Program.Basics Paco(paco2 pacotac)