proposition: Lemma eql_dec : forall l l', {eql l l'}+{~eql l l'}.
proof: Proof. move => l l'. rewrite /eql. case: (nR_dec l l') => h. right. case => h1 _. by apply:h1. case: (nS_dec l l') => h'. right. case => _. by apply. left. split => hn. by apply: h. by apply: h'. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)