. conv =>
    right; rw [isSome_iff_exists]; congr
    intro; unfold constrRun; rw [pbind_eq_some]
  constructor
  . intro h
    rw [del_star_curried, bind_eq_bind, hq', some_bind] at h
    have ⟨r', hr'⟩ := Option.isSome_iff_exists.mp $
      del_star_curried_isSome_iff_constrRun_isSome.mp h
    refine' .intro (.step _ _ r' rfl) ⟨q', hq', _⟩
    simp [toNFA]; assumption
    simp [bind_eq_bind]; assumption
  . intro ⟨r, q', HQ', h⟩
    simp [del_star_curried, bind_eq_bind, hq']
    apply del_star_curried_isSome_iff_constrRun_isSome.mpr
    rw [isSome_iff_exists]; simp [hq'] at HQ'; rw [HQ']
    simp [bind_eq_bind] at h; have ⟨r', _, _⟩ := h
    exists r'
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
no goals