case cons mid tail =>
  cases inferredShape head <;> simp [bind, Option.bind]
  cases inferredShape (.nested (mid :: tail)) <;> simp [Option.bind]
  case some.some s1 s2 =>
    cases s2 <;> simp
    case cons s2_head s2_tail =>
      apply dite (s1 = s2_tail) <;> intros H <;> simp [H]
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
no goals