proposition: Lemma connectedP : reflect (connected A) (connectedb).
proof: Proof. apply: (iffP forallP) => H y; first by move/dec_eq: (H y). apply/dec_eq. case (H y) => x Hx. by exists x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph finfun finset generic_quotient) RegLang(misc languages dfa)