proposition: Lemma bound_ext_subst_term {k sigma1 sigma2 s} : bound k s -> (forall n, n < k -> sigma1 n = sigma2 n) -> subst sigma1 s = subst sigma2 s.
proof: Proof. elim: s k sigma1 sigma2. - move=> > /boundE /= ?. by apply. - move=> ? IH1 ? IH2 k sigma1 sigma2 /boundE + ? /=. move=> [/IH1] => /(_ sigma1 sigma2) ->; first done. by move=> /IH2 => /(_ sigma1 sigma2) ->. - move=> ? IH k sigma1 sigma2 /boundE /IH {}IH H /=. congr lam. apply: IH. move=> [|n]; first done. move=> /= ?. rewrite H; [lia|done]. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect