proposition: Lemma Bar_fun : forall E , IFinite eqA E -> IFinite eqB (f_set E).
proof: Proof. move => e. elim => [E hp hi]. clear e. apply: cBar => y. case => x h1 h2. apply: (@Bar_gset_incl _ (f_set (Intersection E (neq eqA x)))). by apply: hi. move => b [[a ha1 ha2] hb]. exists a => //. split => //. move => hxa. apply: hb. transitivity (f x). by symmetry. transitivity (f a) => //. by apply: f_compat. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)