cases t
t : Tensor2D
⊢ Tensor2D.transpose (Tensor2D.transpose t) = t
case mk
size0✝ size1✝ : ℕ
data✝ : TensorIndex2D size0✝ size1✝ → ℤ
⊢ Tensor2D.transpose (Tensor2D.transpose { size0 := size0✝, size1 := size1✝, data := data✝ }) =
    { size0 := size0✝, size1 := size1✝, data := data✝ }