proposition: Lemma eq_list_iff_list : forall s s', eqlistA eqA s s' -> eq_list s s'.
proof: Proof. elim => [ | hd tl hi] [ | hd' tl'] //=. - move => h; inversion h. - move => h; inversion h. - move => h; inversion h; subst; clear h. case: (eqA_dec hd hd') => //=. move => _; by apply: hi. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)