proposition: Lemma prespect4_companion clo (RES: prespectful4 clo): clo <5= cpn4 gf.
proof: Proof. intros. eapply compatible'4_companion. apply prespect4_compatible'. apply RES. right. right. apply PR. Qed.
imports: Program.Basics Paco(paco4 pacotac)