cases inferredShape (.nested (mid :: tail)) <;> simp
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail head_shape : List ℕ
⊢ (match inferredShape (nested (mid :: tail)), fun s2 =>
        match s2 with
        | [] => none
        | head :: tail => if head_shape = tail then some ((head + 1) :: tail) else none with
      | none, x => none
      | some a, b => b a) =
      some (s_head :: s_tail) →
    0 < s_head ∧ head_shape = s_tail ∧ inferredShape (nested (mid :: tail)) = some ((s_head - 1) :: s_tail)
case some
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail head_shape val✝ : List ℕ
⊢ (match val✝ with
      | [] => none
      | head :: tail => if head_shape = tail then some ((head + 1) :: tail) else none) =
      some (s_head :: s_tail) →
    0 < s_head ∧ head_shape = s_tail ∧ val✝ = (s_head - 1) :: s_tail