{ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((x : α) → (s : σ) → motive (EStateM.Result.ok x s)) →
        ((e : ε) → (s : σ) → motive (EStateM.Result.error e s)) → motive x