proposition: Lemma cbv_cbn_ren xi s : cbv_cbn (ren xi s) = ren xi (cbv_cbn s).
proof: Proof. elim: s xi. - done. - move=> ? IH1 ? IH2 xi /=. by rewrite IH1 IH2 !simpl_term. - move=> ? IH xi /=. rewrite IH !simpl_term. congr lam. congr app. congr lam. apply: ext_ren_term. by case. Qed.
imports: Undecidability.LambdaCalculus(Lambda Util.term_facts Util.wCBN_facts) Undecidability(L.Util.L_facts) Coq(Relations Wellfounded.Transitive_Closure List Lia) Coq(ssreflect)