proposition: Lemma set_pair_der_finite: forall E F, Bar (neq sim3) (Prod (set_pair_der E F) bT).
proof: Proof. move => E F. apply: (@Bar_grel_incl _ _ (r_prod nsim2 nwsim)). - by apply set_pair_der_is_finite. rewrite /nsim2 /nsim /r_prod /neq /sim3 /eq_prod /sim => [[[a a'] u]] [[b b'] u']. case: (similar a b) => /=. move => hneq. left; right => hneq2. by apply: hneq. move => _. by left; left. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)