cases s2 <;> simp
head mid : TensorElem
tail : List TensorElem
s1 s2 : List ℕ
⊢ (match s2 with
      | [] => none
      | head :: tail => if s1 = tail then some ((head + 1) :: tail) else none) =
      some [] →
    False
case cons
head mid : TensorElem
tail : List TensorElem
s1 : List ℕ
head✝ : ℕ
tail✝ : List ℕ
⊢ (if s1 = tail✝ then some ((head✝ + 1) :: tail✝) else none) = some [] → False