proposition: Lemma enc_vector_eq X `{encodable X} m (x:Vector.t X m): enc x = enc (Vector.to_list x).
proof: Proof. reflexivity. Qed.
imports: Undecidability.L.Tactics(LTactics GenEncode) Undecidability.L.Datatypes(LNat List.List_basics List.List_eqb LFinType) Undecidability.Shared.Libs.PSL.Vectors.Vectors