proposition: Lemma asimpl_vector_nil A B (f:A -> B) : Vector.map f (Vector.nil A) = Vector.nil B.
proof: Proof. easy. Qed.
imports: Undecidability.FOL.Syntax(Core Facts) Coq.Classes.Init Relation_Definitions Coq.Classes.RelationClasses Coq.Classes.Morphisms Setoid