proposition: Lemma equiv_many_app_L k (v : Vector.t term k) s t : s == t -> many_app s v == many_app t v.
proof: Proof. induction v in s, t |- *; intros H; cbn. - eassumption. - eapply IHv. now rewrite H. Qed.
imports: Undecidability.L(LTactics) Undecidability.Shared.Libs.PSL.Vectors.Vectors Vector List