proposition: Lemma reachabe_s_proof : reachable (dfa_s A).
proof: Proof. apply/dec_eq. exists nil. exact: eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)