proposition: Lemma subst_many_app k (v : Vector.t term k) n u s : subst (many_app s v) n u = many_app (subst s n u) (Vector.map (fun s => subst s n u) v).
proof: Proof. induction v in s |- *; cbn. - reflexivity. - now rewrite IHv. Qed.
imports: Undecidability.L(LTactics) Undecidability.Shared.Libs.PSL.Vectors.Vectors Vector List