proposition: Lemma prespect10_companion clo (RES: prespectful10 clo): clo <11= cpn10 gf.
proof: Proof. intros. eapply compatible'10_companion. apply prespect10_compatible'. apply RES. right. right. apply PR. Qed.
imports: Program.Basics Paco(paco10 pacotac)