proposition: Lemma In_DER1 : forall f f' v Y, (f,f',v) \in Y -> InA sim_dec3 (DER Y) (der true f, der true f',true::v).
proof: Proof. move => f f' v; elim => [ | [[hdl hdr] s] tl hi] //. rewrite in_cons. case/orP. - by move => heq; rewrite -(eqP heq) {1}/DER -/DER InA_hd. - move => hIn. rewrite {1}/DER -/DER InA_tl //. rewrite {1}/DER -/DER InA_tl //. by apply: hi. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)