. simp [del_star_curried, hq', Option.bind_eq_bind]
  unfold constrRun
  rw [isNone_iff_eq_none, pbind_eq_none]
  assumption; intros; assumption
case none
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
hq' : M.δ (q, x) = none
⊢ Option.isSome (del_star_curried M (x :: xs) q) = true ↔ Option.isSome (constrRun (x :: xs) q) = true

case some
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
⊢ Option.isSome (del_star_curried M (x :: xs) q) = true ↔ Option.isSome (constrRun (x :: xs) q) = true
case some
α qs : Type
M : DFA α qs
w : Word { x // x ∈ M.Z }
q : { x // x ∈ M.Q }
x : { x // x ∈ M.Z }
xs : List { x // x ∈ M.Z }
q' : { x // x ∈ M.Q }
hq' : M.δ (q, x) = some q'
⊢ Option.isSome (del_star_curried M (x :: xs) q) = true ↔ Option.isSome (constrRun (x :: xs) q) = true