proposition: Lemma InA_eq : forall l x y, eqA x y -> InA l x = InA l y.
proof: Proof. elim => [ | a tl hi] x y hxy //=. case: (eqA_dec x a) => //=. - move => hxa. case: (eqA_dec y a) => //=. case. transitivity x => //. by symmetry. - move => hneq. case: (eqA_dec y a) => //=. move => hya; case: hneq. by transitivity y. move => _; by rewrite (hi x y hxy). Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)