constructor
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
⊢ w ∈ AcceptedLanguage M ↔ ∃ qf ∈ del_star M (M.q₀, w), qf ∈ M.F
case mp
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
⊢ w ∈ AcceptedLanguage M → ∃ qf ∈ del_star M (M.q₀, w), qf ∈ M.F

case mpr
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
⊢ (∃ qf ∈ del_star M (M.q₀, w), qf ∈ M.F) → w ∈ AcceptedLanguage M