Mechanised Hypersafety Proofs about Structured Data: Extended Version