fact: Fixpoint eq_list (s s':seq A) {struct s} : bool := match s,s' with | [::], [::] => true | hd :: tl, hd' :: tl' => if eqA_dec hd hd' then eq_list tl tl' else false | _ , _ => false end.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)