proposition: Lemma set_pair_der_is_finite: forall E F, Bar (r_prod (r_prod nsim nsim) nwsim) (Prod (set_pair_der E F) bT).
proof: Proof. move => E F. apply (@Bar_gset_incl _ (Prod (Prod (set_of_der E) (set_of_der F)) bT)). apply Bar_gset_prod. apply Bar_gset_prod. by apply finite_number_of_der. by apply finite_number_of_der. apply cBar => x _. apply cBar => y. case => _. by rewrite /nwsim. case => [[e f] s]. rewrite /set_pair_der /= => [[[u sime simf] _]]. split => //. split. by exists u. by exists u. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)