case nil =>
  cases l <;> simp [inferredShape]
  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]
l : List TensorElem
⊢ inferredShape (nested l) = some [] → False
no goals