intros head mid tail s_head s_tail
⊢ ∀ {head mid : TensorElem} {tail : List TensorElem} {s_head : ℕ} {s_tail : List ℕ},
    inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail) →
      s_head > 0 ∧
        inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail)
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail : List ℕ
⊢ inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail) →
    s_head > 0 ∧ inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail)