intros s_head s_tail H
head : TensorElem
tail : List TensorElem
ih :
  ∀ {head : ℕ} {tail_1 : List ℕ},
    inferredShape (nested tail) = some (head :: tail_1) →
      head = List.length tail ∧ (List.all tail fun x => decide (inferredShape x = some tail_1)) = true
⊢ ∀ {head_1 : ℕ} {tail_1 : List ℕ},
    inferredShape (nested (head :: tail)) = some (head_1 :: tail_1) →
      head_1 = Nat.succ (List.length tail) ∧
        inferredShape head = some tail_1 ∧ ∀ (x : TensorElem), x ∈ tail → inferredShape x = some tail_1
head : TensorElem
tail : List TensorElem
ih :
  ∀ {head : ℕ} {tail_1 : List ℕ},
    inferredShape (nested tail) = some (head :: tail_1) →
      head = List.length tail ∧ (List.all tail fun x => decide (inferredShape x = some tail_1)) = true
s_head : ℕ
s_tail : List ℕ
H : inferredShape (nested (head :: tail)) = some (s_head :: s_tail)
⊢ s_head = Nat.succ (List.length tail) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ tail → inferredShape x = some s_tail