proposition: Theorem eq_term_dec : forall t1 t2:term, {t1 = t2} + {t1 <> t2}.
proof: Proof. intro t1; pattern t1; apply term_rec3. intro x1; destruct t2 as [ x2 | f2 l2]. destruct (eq_variable_dec x1 x2) as [x1_eq_x2 | x1_diff_x2]. left; subst; trivial. right; intro H; apply x1_diff_x2; inversion H; trivial. right; discriminate. intros f1 l1 Hrec t2; destruct t2 as [x2 | f2 l2]. right; discriminate. destruct (eq_symbol_dec f1 f2) as [f1_eq_f2 | f1_diff_f2]. subst; assert (Hrec_list : forall l2, {l1 = l2} + {l1 <> l2}). clear f2 l2; induction l1 as [ | a1 l1]. intro l2; destruct l2 as [ | a2 l2]; [left; trivial | right; discriminate]. intro l2; destruct l2 as [ | a2 l2]. right; discriminate. assert (In_a1 : In a1 (a1 :: l1)). left; trivial. destruct (Hrec a1 In_a1 a2) as [a1_eq_a2 | a1_diff_a2]. assert (Hrec_l1 : forall t, In t l1 -> forall t2, {t = t2} + {t <> t2}). intros; apply Hrec; right; trivial. subst; destruct (IHl1 Hrec_l1 l2) as [l1_eq_l2 | l1_diff_l2]; [ left; subst | right; intro H; apply l1_diff_l2; inversion H] ; trivial. right; intro H; apply a1_diff_a2; inversion H; trivial. destruct (Hrec_list l2) as [l1_eq_l2 | l1_diff_l2]; [ left; subst | right; intro H; apply l1_diff_l2; inversion H] ; trivial. right; intro H; apply f1_diff_f2; inversion H; trivial. Qed.
imports: List more_list list_permut list_set Arith