Fill in the proof of `Contiguous1.contiguous2`, which is the sorry in line 120 in #10.
Fill in the proof of
Contiguous1.contiguous2, which is the sorry in line 120 in #10.