intro H
l : List TensorElem
s_head : ℕ
s_tail : List ℕ
⊢ inferredShape (nested l) = some (s_head :: s_tail) → s_head = List.length l
l : List TensorElem
s_head : ℕ
s_tail : List ℕ
H : inferredShape (nested l) = some (s_head :: s_tail)
⊢ s_head = List.length l