proposition: Lemma Bar_grel_union : forall (E:gset A) (R1 R2 :grel A), Bar R1 E -> Bar R2 E -> Bar (r_union R1 R2) E.
proof: Proof. move => e R1 R2. elim => [e' hp hi]; clear e. move => h. elim :h hp hi => [E hp2 hi2] hp hi; clear e'. apply cBar => a ha. apply: (@Bar_gset_incl (Union (Intersection E (R1 a)) (Intersection E (R2 a)))). apply: Bar_gset_union. + apply: hi ; [done | ]. apply: (@Bar_gset_incl E). apply cBar => b hb. by apply: hp2. by move => x []. + apply: hi2 ; first done. move => x [h1 h2]. apply : (@Bar_gset_incl (Intersection E (R1 x))). by apply: hp. move => y [[] ]. by split. move => x [h1 h2] hB. apply: (@Bar_gset_incl (Intersection E (R1 x))). apply: hi; first done. apply: (@Bar_gset_incl E). by apply:cBar. by move => x' []. by move => y [ [] ]; split. move => x [h1 []]. move => hr1; left. by split. move => hr2; right. by split. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)