∀ {motive : (a : String) → (a_1 : String.Pos.Raw) → String.Pos.Raw.Valid a a_1 → Prop},
  (∀ (cs cs' : List Char) {p : String.Pos.Raw} (hp : p.byteIdx = String.utf8Len cs),
      motive (String.ofList (cs ++ cs')) p ⋯) →
    ∀ {a : String} {a_1 : String.Pos.Raw} (t : String.Pos.Raw.Valid a a_1), motive a a_1 t