(motive : EStateM.Result Unit ℕ Unit → Sort u_1) →
  (x : EStateM.Result Unit ℕ Unit) →
    ((a : Unit) → (a_1 : ℕ) → motive (EStateM.Result.ok a a_1)) →
      ((a : Unit) → (a_1 : ℕ) → motive (EStateM.Result.error a a_1)) → motive x