{K : Type u_1} →
  (motive : Stream'.Seq (GenContFract.Pair K) → ℕ → Sort u_2) →
    (x : Stream'.Seq (GenContFract.Pair K)) →
      (x_1 : ℕ) →
        ((x : Stream'.Seq (GenContFract.Pair K)) → motive x 0) →
          ((s : Stream'.Seq (GenContFract.Pair K)) → (n : ℕ) → motive s n.succ) → motive x x_1