∀ {ε σ α : Type} (motive : EST.Out ε σ α → Sort u_1) (a : α) (s : Void σ)
  (h_1 : (a : α) → (s : Void σ) → motive (EST.Out.ok a s)) (h_2 : (e : ε) → (s : Void σ) → motive (EST.Out.error e s)),
  (match EST.Out.ok a s with
    | EST.Out.ok a s => h_1 a s
    | EST.Out.error e s => h_2 e s) =
    h_1 a s