proposition: Fact in_fot_inv s v w : @in_fot s v = @in_fot s w -> v = w.
proof: Proof. Proof using eq_syms_dec. intros H; destruct in_fot_inv_dep with (1 := H) as (E & H1). rewrite (UIP_dec eq_syms_dec E eq_refl) in H1; 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)