proposition: Lemma prespect1_companion clo (RES: prespectful1 clo): clo <2= cpn1 gf.
proof: Proof. intros. eapply compatible'1_companion. apply prespect1_compatible'. apply RES. right. right. apply PR. Qed.
imports: Program.Basics Paco(paco1 pacotac)