proposition: Lemma prespect6_companion clo (RES: prespectful6 clo): clo <7= cpn6 gf.
proof: Proof. intros. eapply compatible'6_companion. apply prespect6_compatible'. apply RES. right. right. apply PR. Qed.
imports: Program.Basics Paco(paco6 pacotac)