constructor
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
ih :
  s_head - 1 = List.length (mid :: tail) ∧
    (List.all (mid :: tail) fun x => decide (inferredShape x = some s_tail)) = true
⊢ s_head = Nat.succ (List.length (mid :: tail)) ∧
    inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ mid :: tail → inferredShape x = some s_tail
case left
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
ih :
  s_head - 1 = List.length (mid :: tail) ∧
    (List.all (mid :: tail) fun x => decide (inferredShape x = some s_tail)) = true
⊢ s_head = Nat.succ (List.length (mid :: tail))

case right
head : TensorElem
s_head : ℕ
s_tail : List ℕ
mid : TensorElem
tail : List TensorElem
H : inferredShape (nested (head :: mid :: tail)) = some (s_head :: s_tail)
H' : s_head > 0 ∧
  inferredShape head = some s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail) :=
  inferredShape_cons_inv H
ih :
  s_head - 1 = List.length (mid :: tail) ∧
    (List.all (mid :: tail) fun x => decide (inferredShape x = some s_tail)) = true
⊢ inferredShape head = some s_tail ∧ ∀ (x : TensorElem), x ∈ mid :: tail → inferredShape x = some s_tail