proposition: Lemma prespect2_companion clo (RES: prespectful2 clo): clo <3= cpn2 gf.
proof: Proof. intros. eapply compatible'2_companion. apply prespect2_compatible'. apply RES. right. right. apply PR. Qed.
imports: Program.Basics Paco(paco2 pacotac)