proposition: Lemma Set_of_der_compat: forall E F, E_compat sim3 (Prod (set_pair_der E F) bT).
proof: Proof. rewrite /E_compat /set_pair_der => E F [[e f] s] [[e' f'] s'] [[] ]. rewrite /sim => h1 h2 _ [[u h3 h4] _]. split => //. exists u. - transitivity e => //; by symmetry. transitivity f => //; by symmetry. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)