by
  intro A n xs ys
  exact ⟨Hunch.ChunkedSequence.concat_contents A xs ys, Hunch.ChunkedSequence.split_roundtrip A n xs, Hunch.ChunkedSequence.measure_correct A xs⟩