proposition: Lemma reachable_trans_proof (x : reachable_type) a : reachable (dfa_trans (val x) a).
proof: Proof. apply/dec_eq. case/dec_eq : (svalP x) => /= y /eqP <-. exists (y++[::a]). by rewrite delta_cat. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)