proposition: Fact Σ_fin_finite_rels : finite_t (rels Σ').
proof: Proof. set (f r Hr := exist Re r (proj2 (HRe r) Hr)). exists (list_in_map lr f). intros (r & Hr). replace (exist Re r Hr) with (f r (proj1 (HRe r) Hr)). + 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)