Theorem: List.NonEmpty.empty_absurd (MLIR/Util/KDTensor.lean)

State before:
α : Type
CONTRA : NonEmpty []
⊢ False
Tactic:
cases CONTRA
State after:
no goals