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