proposition: Lemma prespect5_companion clo (RES: prespectful5 clo): clo <6= cpn5 gf.
proof: Proof. intros. eapply compatible'5_companion. apply prespect5_compatible'. apply RES. right. right. apply PR. Qed.
imports: Program.Basics Paco(paco5 pacotac)