proposition: Lemma InA_inv : forall (T:eqType) (eqT: grel T) (hE: Equivalence eqT) (hdec: forall x y, {eqT x y}+{~eqT x y}), forall Y e, InA hdec Y e -> exists2 f, (f \in Y) & eqT f e.
proof: Proof. move => T eqT hE hdec. elim => [ | hd tl hi] e //=. case: (hdec e hd) => //=. - move => heq _. exists hd. by rewrite in_cons; apply/orP; left. by symmetry. - move => _ h. case: (hi e h) => f h1 h2. exists f => //. by rewrite in_cons h1 orbT. Defined.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)