proposition: Lemma gpaco1_init clo (WCMP: wcompatible1 gf clo): gpaco1 gf clo bot1 bot1 <1= paco1 gf bot1.
proof: Proof. intros. eapply gpaco1_compat_init. - apply wcompat1_compat, WCMP. apply gf_mon. - eapply gpaco1_mon_bot. apply PR. apply gf_mon. intros; apply PR0. intros. apply gpaco1_clo, PR0. Qed.
imports: Program.Basics Paco(paco1 pacotac)