proposition: Lemma Bar_gset_incl : forall (F:gset A) (R:grel A), Bar R F -> forall (E:gset A) , Included E F -> Bar R E.
proof: Proof. move => f R. elim => [F hp hi] E hIncl. clear f. apply: cBar => a hIna. apply: (hi a). by apply :hIncl. move => x [h1 h2]. split => //. by apply: hIncl. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)