proposition: Lemma cpn13_cpn r: cpn13 (cpn13 r) <13= cpn13 r.
proof: Proof. intros. apply cpn13_gupaco, gpaco13_gupaco, gpaco13_clo. apply gf_mon. eapply cpn13_mon, gpaco13_clo. apply PR. Qed.
imports: Program.Basics Paco(paco13 pacotac)