{s : String} →
  {p : s.Pos} →
    {t₁ t₂ : String} →
      {motive : p.Splits t₁ t₂ → Sort u} →
        (t : p.Splits t₁ t₂) →
          ((eq_append : s = t₁ ++ t₂) → (offset_eq_rawEndPos : p.offset = t₁.rawEndPos) → motive ⋯) → motive t