proposition: Lemma subst_many_lam k n u s : subst (many_lam k s) n u = many_lam k (subst s (k + n) u).
proof: Proof. induction k in n |- *; cbn. - reflexivity. - f_equal. rewrite IHk. repeat f_equal. lia. Qed.
imports: Undecidability.L(LTactics) Undecidability.Shared.Libs.PSL.Vectors.Vectors Vector List