proposition: Lemma gpred_listP : forall E l (H:E_compat E), gpred_list E l <-> (forall x, InA l x -> E x).
proof: Proof. rewrite /E_compat. move => E. elim => [ | hd tl hi] HE //=; split. - case => hhd htl x. case: (eqA_dec x hd) => //=. move => heq _. apply : (@HE hd x) => //. by symmetry. move => _. by apply hi. - move => h; split. apply:h . case: (eqA_dec hd hd) => //=. by case; reflexivity. apply hi. exact HE. move => z hz. apply: h. by case: (eqA_dec z hd). Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)