case cons head tail =>
  cases tail <;> simp [inferredShape]
  case nil =>
    cases inferredShape head <;> simp [bind, Option.bind]
  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 : TensorElem
tail : List TensorElem
⊢ inferredShape (nested (head :: tail)) = some [] → False
no goals