cases l <;> simp [inferredShape]
l : List TensorElem
⊢ inferredShape (nested l) = some [] → False
case cons
head✝ : TensorElem
tail✝ : List TensorElem
⊢ inferredShape (nested (head✝ :: tail✝)) = some [] → False