proposition: Lemma Sort_InA_eq : forall xs ys, Sort xs -> Sort ys -> (forall a, InA (@eq _) a xs <-> InA (@eq _) a ys) -> xs = ys.
proof: Proof. intros xs ys ? ? ?. cut (eqlistA (@eq _) xs ys). auto using eqlist_eq. apply SetoidList.SortA_equivlistA_eqlistA with (ltA := ltA); eauto. apply eq_equivalence. firstorder. reduce. subst. split; auto. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Metalib.CoqUniquenessTac