{α : Type u_1} →
  (motive : Batteries.DList α × Stream'.WSeq α → Sort u_2) →
    (x : Batteries.DList α × Stream'.WSeq α) →
      ((l : Batteries.DList α) → (s : Stream'.WSeq α) → motive (l, s)) → motive x