{α : Type} →
  (motive : Option α × Bool → Sort u_1) →
    (__discr : Option α × Bool) →
      ((val : α) → (shouldDequeue : Bool) → motive (some val, shouldDequeue)) →
        ((x : Option α × Bool) → motive x) → motive __discr