proposition: Lemma InA_eq2 : forall l l' x, eq_list l l' -> InA l x = InA l' x.
proof: Proof. elim. by case => //=. move => hd tl hi. case => //=. move => hd' tl' x. case: (eqA_dec hd hd') => //= heq1 htl. case: (eqA_dec x hd) => //=. move => heq . case: (eqA_dec x hd') => //=. case. by transitivity hd. move => hneq. case: (eqA_dec x hd') => //=. move => heq2. case: hneq. transitivity hd' => //. by symmetry. move => hn; by apply: (hi tl' x). Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)