proposition: Lemma gpaco4_init clo (WCMP: wcompatible4 gf clo): gpaco4 gf clo bot4 bot4 <4= paco4 gf bot4.
proof: Proof. intros. eapply gpaco4_compat_init. - apply wcompat4_compat, WCMP. apply gf_mon. - eapply gpaco4_mon_bot. apply PR. apply gf_mon. intros; apply PR0. intros. apply gpaco4_clo, PR0. Qed.
imports: Program.Basics Paco(paco4 pacotac)