proposition: Lemma prespect9_companion clo (RES: prespectful9 clo): clo <10= cpn9 gf.
proof: Proof. intros. eapply compatible'9_companion. apply prespect9_compatible'. apply RES. right. right. apply PR. Qed.
imports: Program.Basics Paco(paco9 pacotac)