proposition: Lemma apply_to_equiv' s t {X k} (v : Vector.t X k) `{encodable X} : s == t -> apply_to s v == apply_to t v.
proof: Proof. eapply equiv_many_app_L. Qed.
imports: Undecidability.Shared.Libs.PSL(Vectors) Coq(Vector List) Undecidability.L(L LTactics L_facts Functions.Eval) Undecidability.L.Util(NaryApp)