proposition: Lemma eq_term_dec (s t : term) : (s = t) + (s <> t).
proof: Proof. revert t. induction s; intros t; destruct t; try(right; intros H; inv H; fail). - decide (n = n0). left. congruence. right. congruence. - destruct (IHs1 t1), (IHs2 t2); try (right; congruence). left. congruence. - destruct (IHs t). left; congruence. right; congruence. Qed.
imports: Coq.Logic.ConstructiveEpsilon