proposition: Theorem eq_fo_term_dec : discrete fo_term.
proof: Proof. Proof using eq_syms_dec. intros t; induction t as [ i | s v IHv ]; intros [ j | s' w ]. + destruct (eq_nat_dec i j) as [ -> | H ]; [ left | right ]; auto. contradict H; inversion H; auto. + right; discriminate. + right; discriminate. + destruct (eq_syms_dec s s') as [ <- | H ]. * destruct list_dec with (P := fun p => vec_pos v p <> vec_pos w p) (Q := fun p => vec_pos v p = vec_pos w p) (l := pos_list (ar_syms s)) as [ (p & _ & H) | H ]. - intros p; generalize (IHv p (vec_pos w p)); unfold decidable; tauto. - right; contradict H; f_equal; revert H; apply in_fot_inv. - left; f_equal; apply vec_pos_ext; intros p. apply H, pos_list_prop. * right; contradict H; inversion H; auto. Qed.
imports: List Arith Lia Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils decidable fol_ops fo_sig)