proposition: Lemma gpaco3_init clo (WCMP: wcompatible3 gf clo): gpaco3 gf clo bot3 bot3 <3= paco3 gf bot3.
proof: Proof. intros. eapply gpaco3_compat_init. - apply wcompat3_compat, WCMP. apply gf_mon. - eapply gpaco3_mon_bot. apply PR. apply gf_mon. intros; apply PR0. intros. apply gpaco3_clo, PR0. Qed.
imports: Program.Basics Paco(paco3 pacotac)