proposition: Lemma Bar_gset_prod: forall (E:gset A) (Ra:grel A) (Rb: grel B), Bar Ra E -> forall F, Bar Rb F -> Bar (r_prod Ra Rb) (Prod E F).
proof: Proof. move => e Ra Rb. elim => [ E hp hi] f. elim => [ F hp2 hi2]. clear f e. apply cBar => [[a b] [h1 h2]]. apply: (@Bar_gset_incl _ (Union (Prod (Intersection E (Ra a)) F) (Prod E (Intersection F (Rb b))))). apply: Bar_gset_union. by apply : hi. by apply : hi2. clear hp hi hp2 hi2. case => x y [] [hp1 hp2] [hL | hR]. left. by split. 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)