I want to prove the following theorem on two pairs of type TR:
Definition s:= nat.
Definition d:= nat.
Definition c:= nat.
Definition p:= nat.
Inductive rt: Set :=
|al : rt
|bl : rt.
Definition TR: Set :=
rt* s*d* c* p.
Implicit Types m n : TR.
Theorem eq_TR_dec : forall n m, {n = m} + {n <> m}.
For now, the proof of this theorem begins by intros n. destruct n. destruct m. But I cannot figure out the best tactic to prove this theorem. Any idea how should I prove this theorem? Thank you