case some.some s1 s2 =>
  cases s2 <;> simp
  case cons s2_head s2_tail =>
    apply dite (s1 = s2_tail) <;> intros H <;> simp [H]
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
no goals