proposition: Lemma prespect11_companion clo (RES: prespectful11 clo): clo <12= cpn11 gf.
proof: Proof. intros. eapply compatible'11_companion. apply prespect11_compatible'. apply RES. right. right. apply PR. Qed.
imports: Program.Basics Paco(paco11 pacotac)