proposition: Lemma eqlist_eq : forall (xs ys : list A), eqlistA (@eq _) xs ys -> xs = ys.
proof: Proof. induction xs; destruct ys; inversion 1; f_equal; auto. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Metalib.CoqUniquenessTac