case H0
α : Type u
σ σ' : Type v
M : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
⊢ evalFrom M ∅ [] = ∅

case H1
α : Type u
σ σ' : Type v
M : εNFA α σ
S : Set σ
x✝ : List α
s : σ
a✝ : α
x : List α
a : α
ih : evalFrom M ∅ x = ∅
⊢ evalFrom M ∅ (x ++ [a]) = ∅
α : Type u
σ σ' : Type v
M : εNFA α σ
S : Set σ
x✝ : List α
s : σ
a : α
x : List α
⊢ evalFrom M ∅ x = ∅
induction' x using List.reverseRecOn with x a ih
no goals
case H0
α : Type u
σ σ' : Type v
M : εNFA α σ
S : Set σ
x : List α
s : σ
a : α
⊢ evalFrom M ∅ [] = ∅
rw [evalFrom_nil, εClosure_empty]
no goals
case H1
α : Type u
σ σ' : Type v
M : εNFA α σ
S : Set σ
x✝ : List α
s : σ
a✝ : α
x : List α
a : α
ih : evalFrom M ∅ x = ∅
⊢ evalFrom M ∅ (x ++ [a]) = ∅
rw [evalFrom_append_singleton, ih, stepSet_empty]