proposition: Lemma wrespect14_companion clo (RES: wrespectful14 clo): clo <15= cpn14 gf.
proof: Proof. intros. eapply wrespect14_compatible' in RES. eapply (@compatible'14_companion (rclo14 clo)) in RES; [apply RES|]. eapply rclo14_clo_base, PR. Qed.
imports: Program.Basics Paco(paco14 pacotac)