proposition: Lemma sort_equivlistA_eqlistA : forall l l' : list (key*elt), sort ltk l -> sort ltk l' -> equivlistA eqke l l' -> eqlistA eqke l l'.
proof: Proof. apply SortA_equivlistA_eqlistA; eauto with *. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)