proposition: Lemma prespect7_companion clo (RES: prespectful7 clo): clo <8= cpn7 gf.
proof: Proof. intros. eapply compatible'7_companion. apply prespect7_compatible'. apply RES. right. right. apply PR. Qed.
imports: Program.Basics Paco(paco7 pacotac)