proposition: Lemma prespect14_companion clo (RES: prespectful14 clo): clo <15= cpn14 gf.
proof: Proof. intros. eapply compatible'14_companion. apply prespect14_compatible'. apply RES. right. right. apply PR. Qed.
imports: Program.Basics Paco(paco14 pacotac)