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