proposition: Lemma InA_tl : forall a b l, InA l a -> InA (b::l) a.
proof: Proof. move => a b l h /=. by case: (eqA_dec a b). Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)