cases tail <;> simp [inferredShape]
head : TensorElem
tail : List TensorElem
⊢ inferredShape (nested (head :: tail)) = some [] → False
case nil
head : TensorElem
⊢ (do
        let __do_lift ← inferredShape head
        some (1 :: __do_lift)) =
      some [] →
    False

case cons
head head✝ : TensorElem
tail✝ : List TensorElem
⊢ (do
        let s1 ← inferredShape head
        let s2 ← inferredShape (nested (head✝ :: tail✝))
        match s2 with
          | [] => none
          | head :: tail => if s1 = tail then some ((head + 1) :: tail) else none) =
      some [] →
    False