case mk size0 size1 data => {
 simp[Tensor2D.transpose];
 simp[transpose_index_twice_is_id];
}
size0 size1 : ℕ
data : TensorIndex2D size0 size1 → ℤ
⊢ Tensor2D.transpose (Tensor2D.transpose { size0 := size0, size1 := size1, data := data }) =
    { size0 := size0, size1 := size1, data := data }
no goals