∀ (motive : String.Legacy.Iterator → Sort u_1) (s : String) (i : String.Pos.Raw)
  (h_1 : (s : String) → (i : String.Pos.Raw) → motive { s := s, i := i }),
  (match { s := s, i := i } with
    | { s := s, i := i } => h_1 s i) =
    h_1 s i