proposition: Lemma ext_subst_term sigma1 sigma2 t : (forall n, sigma1 n = sigma2 n) -> subst sigma1 t = subst sigma2 t.
proof: Proof. elim: t sigma1 sigma2. - by move=> > /= ?. - move=> ? IH1 ? IH2 ?? Hsigma /=. congr app; [by apply: IH1 | by apply: IH2]. - move=> ? IH > Hsigma /=. congr lam. apply: IH. case; first done. move=> ?. by rewrite /= Hsigma. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect