cases inferredShape head <;> simp [bind, Option.bind]
head mid : TensorElem
tail : List TensorElem
⊢ (do
        let s1 ← inferredShape head
        let s2 ← inferredShape (nested (mid :: tail))
        match s2 with
          | [] => none
          | head :: tail => if s1 = tail then some ((head + 1) :: tail) else none) =
      some [] →
    False
case some
head mid : TensorElem
tail : List TensorElem
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 [] →
    False