proposition: Lemma compareList_refl : forall l, compareList l l = Eq.
proof: Proof. elim => [ | hd tl hi] //=. by rewrite (compare_refl hd). Qed.
imports: Coq(RelationClasses Setoid Morphisms) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue regexp finite_der equiv)