proposition: Lemma prespect0_companion clo (RES: prespectful0 clo): clo <1= cpn0 gf.
proof: Proof. intros. eapply compatible'0_companion. apply prespect0_compatible'. apply RES. right. right. apply PR. Qed.
imports: Program.Basics Paco(paco0 pacotac)