proposition: Lemma gpaco13_init clo (WCMP: wcompatible13 gf clo): gpaco13 gf clo bot13 bot13 <13= paco13 gf bot13.
proof: Proof. intros. eapply gpaco13_compat_init. - apply wcompat13_compat, WCMP. apply gf_mon. - eapply gpaco13_mon_bot. apply PR. apply gf_mon. intros; apply PR0. intros. apply gpaco13_clo, PR0. Qed.
imports: Program.Basics Paco(paco13 pacotac)