proposition: Lemma InA_cat : forall l l' x, InA (l++l') x = InA l x || InA l' x.
proof: Proof. elim => [ | hd tl hi] l' x //=. by case: (eqA_dec x hd) => h //=. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)