proposition: Lemma wrespect13_companion clo (RES: wrespectful13 clo): clo <14= cpn13 gf.
proof: Proof. intros. eapply wrespect13_compatible' in RES. eapply (@compatible'13_companion (rclo13 clo)) in RES; [apply RES|]. eapply rclo13_clo_base, PR. Qed.
imports: Program.Basics Paco(paco13 pacotac)