proposition: Lemma ren_as_subst_term xi t : ren xi t = subst (funcomp var xi) t.
proof: Proof. elim: t xi => /=. - done. - move=> ? IH1 ? IH2 ?. by rewrite IH1 IH2. - move=> ? IH ?. rewrite IH. congr lam. apply: ext_subst_term. by case. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect