cases tail_shape <;> simp
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail head_shape tail_shape : List ℕ
⊢ (match tail_shape with
      | [] => none
      | head :: tail => if head_shape = tail then some ((head + 1) :: tail) else none) =
      some (s_head :: s_tail) →
    0 < s_head ∧ head_shape = s_tail ∧ tail_shape = (s_head - 1) :: s_tail
case cons
head mid : TensorElem
tail : List TensorElem
s_head : ℕ
s_tail head_shape : List ℕ
head✝ : ℕ
tail✝ : List ℕ
⊢ (if head_shape = tail✝ then some ((head✝ + 1) :: tail✝) else none) = some (s_head :: s_tail) →
    0 < s_head ∧ head_shape = s_tail ∧ head✝ = s_head - 1 ∧ tail✝ = s_tail