{ε α : Type} →
  (motive : List α × Option ε × Bool → Sort u_1) →
    (__discr : List α × Option ε × Bool) →
      ((tl : List α) → (e? : Option ε) → (isComplete : Bool) → motive (tl, e?, isComplete)) → motive __discr