proposition: Lemma L_subst_Lambda_subst s k t : L.closed t -> L.subst s k t = subst (fun n => if Nat.eqb n k then t else var n) s.
proof: Proof. move=> Ht. elim: s k. - done. - move=> ? IH1 ? IH2 ? /=. by rewrite IH1 IH2. - move=> ? IH k /=. rewrite IH. congr lam. apply: ext_subst_term. move=> [|n] /=; first done. case: (Nat.eqb n k); last done. by rewrite (ren_closed Ht). Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect