proposition: Lemma eql_iff_list : forall s s', eql s s' <-> equivlistA eqA s s'.
proof: Proof. move => s s'; split. - move/eql_elim => heql. rewrite /equivlistA. move => x; split => h. apply/InA2P. apply heql. by apply/InA2P. apply/InA2P. apply heql. by apply/InA2P. - rewrite /equivlistA => heq. apply/eql_elim => x; split => h. apply/InA2P. apply heq. by apply/InA2P. apply/InA2P. apply heq. by apply/InA2P. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)