proposition: Lemma Finite_Union_is_finite : forall (R:grel A) (n:nat) (Es: prodn (gset A) n), pred_prodn (Bar R) Es -> Bar R (Finite_Union Es).
proof: Proof. move => R. elim => [ | p hi] /=. - move => _ _ . by apply: Bar_Empty_gset. - move => [e Es] [h1 h2]. apply: Bar_gset_union ; first done. by apply: hi. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)