assumption
case final.right.h.right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
a✝¹ : { x // x ∈ (toNFA (fromNFA M)).Q }
a✝ : Word { x // x ∈ (toNFA (fromNFA M)).Z }
self✝ : { x // x ∈ (toNFA (fromNFA M)).Q }
h' : ↑a✝¹ ⊆ ↑self✝
h✝ : a✝ = ε
h : a✝¹ ∈ Finset.attach Finset.univ ∧ ∃ q ∈ ↑a✝¹, q ∈ M.F
left✝¹ : a✝¹ ∈ Finset.attach Finset.univ
q : { x // x ∈ M.Q }
left✝ : q ∈ ↑a✝¹
right✝ : q ∈ M.F
⊢ { val := ↑q, property := ⋯ } ∈ M.F
no goals