proposition: Lemma Bar_Empty_gset: forall R:grel A, Bar R (@Empty_gset A).
proof: Proof. move => R. apply : cBar => a ha. by case: (@Empty_gset_inv A a). Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)