∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Prop) (x : EStateM.Result ε σ α),
  (∀ (a : α) (a_1 : σ), motive (EStateM.Result.ok a a_1)) →
    (∀ (a : ε) (a_1 : σ), motive (EStateM.Result.error a a_1)) → motive x