proposition: Fact Σ_fin_finite_syms : finite_t (syms Σ').
proof: Proof. set (f s Hs := exist Fn s (proj2 (HFn s) Hs)). exists (list_in_map ls f). intros (s & Hs). replace (exist Fn s Hs) with (f s (proj1 (HFn s) Hs)). + apply In_list_in_map. + unfold f; f_equal; apply eq_bool_pirr. Qed.
imports: List Arith Bool Lia Eqdep_dec Max 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 fo_terms fo_logic fo_sat)