∀ {s : String.Slice} {p : s.Pos} {off : String.Pos.Raw}
  (motive : off ≤ p.offset ∧ String.Pos.Raw.IsValidForSlice s off → Prop)
  (x : off ≤ p.offset ∧ String.Pos.Raw.IsValidForSlice s off),
  (∀ (h₁ : off ≤ p.offset) (h₂ : off ≤ s.rawEndPos)
      (h₃ : String.Pos.Raw.IsValid s.str (off.offsetBy s.startInclusive.offset)), motive ⋯) →
    motive x