case cons s_head s_tail =>
  intro H
  let H' := inferredShape_list H
  exact H'.1
l : List TensorElem
s_head : ℕ
s_tail : List ℕ
⊢ inferredShape (nested l) = some (s_head :: s_tail) → s_head = List.length l
no goals