proposition: Lemma Bar_grel_incl : forall E (R R':grel A), Bar R E -> r_incl R' R -> Bar R' E.
proof: Proof. move => e R R'. elim => [E hp hi] hincl. clear e. apply cBar => a ha. apply : (@Bar_gset_incl (Intersection E (R a))). by apply: hi. move => x [h1 h2]. split => //. move: (hincl a) => hh. by apply : hh. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)