How do I unfold match in the following example?

Stream: new members

[Z. Wu]

In the following code, it is obvious that the example holds because we only care about the first element in the tuple returned by the match. But it seems like simp won't go through in this scenario. If I induction ht, then it works fine, which makes sense.

But if match has many more terms, it would be a nightmare because I have to invoke induction on each of the term. Is there a tactic that goes through in this scenario?

inductive Seqx {α: Type} : α -> Type where
| cons (s s': α): Seqx s' -> Seqx s

example {α: Type} (s s': α) (ht: Seqx s): s = (match s, ht with | sm, Seqx.cons _ q sn => (sm, q)).1  := by
  -- induction ht automagically works
  sorry