proposition: Lemma prespect3_companion clo (RES: prespectful3 clo): clo <4= cpn3 gf.
proof: Proof. intros. eapply compatible'3_companion. apply prespect3_compatible'. apply RES. right. right. apply PR. Qed.
imports: Program.Basics Paco(paco3 pacotac)