proposition: Lemma asimpl_vector_cons A B (f:A -> B) t n v : Vector.map f (@Vector.cons A t n v) = @Vector.cons B (f t) n (Vector.map f v).
proof: Proof. easy. Qed.
imports: Undecidability.FOL.Syntax(Core Facts) Coq.Classes.Init Relation_Definitions Coq.Classes.RelationClasses Coq.Classes.Morphisms Setoid