intro M w
α✝ : Type ?u.32572
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
⊢ let M := canonicalAutomaton nc;
  ∀ (w : Word { x // x ∈ M.Z }), TotalDFA.del_star' M (M.q₀, w) ∈ M.F ↔ w ∈ L
α✝ : Type ?u.32572
L✝ : Language α✝
u v : Word α✝
α : Type
Z : Finset α
L : Language { x // x ∈ Z }
proc : DecisionProcedure L
nc✝ nc : Fintype (Quotient (myhillNerodeEquivalence L))
M : TotalDFA α (Quotient (myhillNerodeEquivalence L)) := canonicalAutomaton nc
w : Word { x // x ∈ M.Z }
⊢ TotalDFA.del_star' M (M.q₀, w) ∈ M.F ↔ w ∈ L