∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (a : α) (s' : σ)
  (h_1 :
    (a_1 : α) → (s'_1 : σ) → EStateM.Result.ok a s' = EStateM.Result.ok a_1 s'_1 → motive (EStateM.Result.ok a_1 s'_1))
  (h_2 :
    (e : ε) → (s'_1 : σ) → EStateM.Result.ok a s' = EStateM.Result.error e s'_1 → motive (EStateM.Result.error e s'_1)),
  (match w : EStateM.Result.ok a s' with
    | EStateM.Result.ok a_1 s'_1 => h_1 a_1 s'_1 w
    | EStateM.Result.error e s'_1 => h_2 e s'_1 w) =
    h_1 a s' ⋯