proposition: Theorem Σsyms_Σnosyms_sound Σ ls A X : fo_form_fin_discr_dec_SAT_in A X -> @fo_form_fin_dec_eq_SAT_in (Σnosyms Σ) (inl tt) eq_refl (Σsyms_Σnosyms ls A) X.
proof: Proof. intros (H0 & M & H1 & H2 & phi & H3). exists (fom_nosyms M), H1; destruct M as (sy,re). exists. { intros [[]|[s|r]]; simpl. + intros; apply H0. + intros; apply H0. + intros; apply H2. } exists. { intros x y; cbv; tauto. } exists phi. unfold Σsyms_Σnosyms; split. + apply fol_rels_are_functions_spec; auto; simpl; try tauto. intros s Hs; split. * intros v x y; simpl; intros; subst; auto. * intros v; exists (sy s v); simpl; auto. + revert H3; apply fol_rem_syms_spec. Qed.
imports: List Arith Bool 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 fol_ops fo_sig utils fo_terms fo_logic fo_sat) Undecidability.Shared.ListAutomation