proposition: Lemma gpaco5_init clo (WCMP: wcompatible5 gf clo): gpaco5 gf clo bot5 bot5 <5= paco5 gf bot5.
proof: Proof. intros. eapply gpaco5_compat_init. - apply wcompat5_compat, WCMP. apply gf_mon. - eapply gpaco5_mon_bot. apply PR. apply gf_mon. intros; apply PR0. intros. apply gpaco5_clo, PR0. Qed.
imports: Program.Basics Paco(paco5 pacotac)