proposition: Lemma Bar_gset_union: forall (E:gset A) (R:grel A), Bar R E -> forall (F:gset A), Bar R F -> Bar R (Union E F).
proof: Proof. move => e R. elim => [E hp hi]; clear e. move => f. elim => [F hp2 hi2]; clear f. apply cBar => a. case => ha. - apply: (@Bar_gset_incl (Union (Intersection E (R a)) F)). by apply: hi. move => x [ [] ]. move => h1 h2. left. by split. move => h1 h2. by right. - apply: (@Bar_gset_incl (Union E (Intersection F (R a)))). by apply: hi2. move => x [[] ]. move => h1 h2. by left. move => h1 h2. 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)