proposition: Lemma eq_list_eql_Eq : forall (l l': seq A), Sorteds l -> Sorteds l' -> eql l l' -> eq_list l l'.
proof: Proof. move => l l' hS1 hS2. move/eql_iff_list => heql. apply eq_list_iff_list. by apply: SortA_equivlistA_eqlistA. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)