proposition: Lemma prespect8_companion clo (RES: prespectful8 clo): clo <9= cpn8 gf.
proof: Proof. intros. eapply compatible'8_companion. apply prespect8_compatible'. apply RES. right. right. apply PR. Qed.
imports: Program.Basics Paco(paco8 pacotac)