proposition: Lemma gpaco0_init clo (WCMP: wcompatible0 gf clo): gpaco0 gf clo bot0 bot0 <0= paco0 gf bot0.
proof: Proof. intros. eapply gpaco0_compat_init. - apply wcompat0_compat, WCMP. apply gf_mon. - eapply gpaco0_mon_bot. apply PR. apply gf_mon. intros; apply PR0. intros. apply gpaco0_clo, PR0. Qed.
imports: Program.Basics Paco(paco0 pacotac)