case cons s2_head s2_tail =>
  apply dite (s1 = s2_tail) <;> intros H <;> simp [H]
head mid : TensorElem
tail : List TensorElem
s1 : List ℕ
s2_head : ℕ
s2_tail : List ℕ
⊢ (if s1 = s2_tail then some ((s2_head + 1) :: s2_tail) else none) = some [] → False
no goals