Theorem: TensorIndex'.empty_dims_is_empty (MLIR/Util/KDTensor.lean)

State before:
index : TensorIndex' []
⊢ index = Empty
Tactic:
cases index
State after:
case Empty

⊢ Empty = Empty

State before:
case Empty

⊢ Empty = Empty
Tactic:
simp
State after:
no goals