proposition: Lemma many_subst_app (s t : term) {k} n (v : Vector.t term k) : many_subst (s t) n v = (many_subst s n v) (many_subst t n v).
proof: Proof. induction v in n, s, t |- *. - reflexivity. - cbn. now rewrite IHv. Qed.
imports: Undecidability.L(LTactics) Undecidability.Shared.Libs.PSL.Vectors.Vectors Vector List