proposition: Lemma lemma6_prime2 : forall E R (x:A), Acc E R x -> Bar (fun x y => R y x) (Intersection E (R^~ x)).
proof: Proof. move => E R x'. elim => [x hP hi]; clear x'. apply: cBar => y. case => h1 h2. apply : (@Bar_gset_incl _ (Intersection E (R^~ y))). - by apply: hi. move => a [] [ha1 ha2] ha3. by split. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)