cases s <;> simp [inferredShape]
l : List TensorElem
s : List ℕ
⊢ inferredShape (nested l) = some s → ∃ tail, s = List.length l :: tail
case nil
l : List TensorElem
⊢ inferredShape (nested l) = some [] → False

case cons
l : List TensorElem
head✝ : ℕ
tail✝ : List ℕ
⊢ inferredShape (nested l) = some (head✝ :: tail✝) → head✝ = List.length l