cases tail
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
case nil
head : TensorElem
s_head : ℕ
s_tail : List ℕ
ih :
  ∀ {head : ℕ} {tail : List ℕ},
    inferredShape (nested []) = some (head :: tail) →
      head = List.length [] ∧ (List.all [] fun x => decide (inferredShape x = some tail)) = true
H : inferredShape (nested [head]) = some (s_head :: s_tail)
⊢ s_head = Nat.succ (List.length []) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ [] → inferredShape x = some s_tail

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