proposition: Lemma apply_to_cons (s : L.term) {k} {X : Type} `{encodable X} (v : Vector.t X k) x : apply_to s (x :: v) = apply_to (L.app s (enc x)) v.
proof: Proof. reflexivity. Qed.
imports: Undecidability.Shared.Libs.PSL(Vectors) Coq(Vector List) Undecidability.L(L LTactics L_facts Functions.Eval) Undecidability.L.Util(NaryApp)