proposition: Lemma many_subst_many_app (s : term) {k} n (ts v : Vector.t term k) : many_subst (many_app s ts) n v = many_app (many_subst s n v) (Vector.map (fun t => many_subst t n v) ts).
proof: Proof. induction v in n, s, ts |- *. - cbn. revert ts. apply case0. reflexivity. - cbn. apply (caseS' ts). cbn. intros. rewrite subst_many_app, IHv. cbn. rewrite many_subst_app. now rewrite Vector.map_map. Qed.
imports: Undecidability.L(LTactics) Undecidability.Shared.Libs.PSL.Vectors.Vectors Vector List