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