proposition: Lemma InA2P : forall x l, reflect (InA2 x l) (InA l x).
proof: Proof. move => x l; apply: (iffP idP); last first. by elim => y l0; rewrite /= /is_left; case: (eqA_dec x y). elim: l => [|hd tl hi] //=. case: (eqA_dec x hd) => /= heq hIn; first by left. by apply SetoidList.InA_cons; right; apply: hi. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)