no goals
α : Type u
σ σ' : Type v
M : εNFA α σ
S✝ : Set σ
x✝ : List α
s : σ
a✝ : α
S : Set σ
x : List α
a : α
⊢ evalFrom M S (x ++ [a]) = stepSet M (evalFrom M S x) a
rw [evalFrom, List.foldl_append, List.foldl_cons, List.foldl_nil]