proposition: Lemma cpn11_cpn r: cpn11 (cpn11 r) <11= cpn11 r.
proof: Proof. intros. apply cpn11_gupaco, gpaco11_gupaco, gpaco11_clo. apply gf_mon. eapply cpn11_mon, gpaco11_clo. apply PR. Qed.
imports: Program.Basics Paco(paco11 pacotac)