proposition: Lemma Empty_gset_inv : forall x, ~ Empty_gset x.
proof: Proof. by move => x; case. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)