proposition: Lemma wrespect12_companion clo (RES: wrespectful12 clo): clo <13= cpn12 gf.
proof: Proof. intros. eapply wrespect12_compatible' in RES. eapply (@compatible'12_companion (rclo12 clo)) in RES; [apply RES|]. eapply rclo12_clo_base, PR. Qed.
imports: Program.Basics Paco(paco12 pacotac)