proposition: Lemma prespect12_companion clo (RES: prespectful12 clo): clo <13= cpn12 gf.
proof: Proof. intros. eapply compatible'12_companion. apply prespect12_compatible'. apply RES. right. right. apply PR. Qed.
imports: Program.Basics Paco(paco12 pacotac)