proposition: Lemma prespect13_companion clo (RES: prespectful13 clo): clo <14= cpn13 gf.
proof: Proof. intros. eapply compatible'13_companion. apply prespect13_compatible'. apply RES. right. right. apply PR. Qed.
imports: Program.Basics Paco(paco13 pacotac)