trivial
case h_1
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
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
heq✝ : inferredShape head = none
H : none = some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail

case h_2
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
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
a✝ : List ℕ
heq✝ : inferredShape head = some a✝
H : (fun __do_lift => some (1 :: __do_lift)) a✝ = some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail
case h_2
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
x✝¹ : Option (List ℕ)
x✝ : List ℕ → Option (List ℕ)
a✝ : List ℕ
heq✝ : inferredShape head = some a✝
H : (fun __do_lift => some (1 :: __do_lift)) a✝ = some (s_head :: s_tail)
⊢ s_head = Nat.succ 0 ∧ inferredShape head = some s_tail