{ε σ α : Type} →
  {motive : EST.Out ε σ α → Sort u} →
    ((a : α) → (a_1 : Void σ) → motive (EST.Out.ok a a_1)) →
      ((a : ε) → (a_1 : Void σ) → motive (EST.Out.error a a_1)) → (t : EST.Out ε σ α) → motive t