{w : ℕ} →
  (s : ℕ) →
    (motive : (s' : ℕ) → s' + 1 < w → 0 < s' + 1 → s = s'.succ → Sort u_1) →
      (s' : ℕ) →
        (hs : s' + 1 < w) →
          (hslt : 0 < s' + 1) →
            (hs0 : s = s'.succ) →
              ((hs : 0 + 1 < w) → (hslt : 0 < 0 + 1) → (hs0 : s = Nat.succ 0) → s' = 0 → motive 0 hs hslt hs0) →
                ((s'' : ℕ) →
                    (hs : s'' + 1 + 1 < w) →
                      (hslt : 0 < s'' + 1 + 1) →
                        (hs0 : s = (s'' + 1).succ) → s' = s''.succ → motive s''.succ hs hslt hs0) →
                  motive s' hs hslt hs0