proposition: Lemma lincl_mem_sim : forall (A:eqType) (eqA: grel A) (hE: Equivalence eqA) (hdec: forall x y, {eqA x y}+{~eqA x y}), forall (l:seq A) a, (a \in l) -> InA hdec l a.
proof: Proof. move => A eqA hE hdec. elim => [ | hd tl hi] //= a. rewrite in_cons; case/orP => hu. - rewrite (eqP hu). case: (hdec hd hd) => //=. case; by reflexivity. - case: (hdec a hd) => //= _. by apply: hi. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)