proposition: Theorem Σ_noeq_sound : fo_form_fin_dec_eq_SAT_in _ H_ae A X -> fo_form_fin_dec_SAT_in (Σ_noeq A) X.
proof: Proof. intros (M & H1 & H2 & HE & phi & H5). exists M, H1, H2, phi; unfold Σ_noeq. rewrite fol_sem_bin_fix; split; auto. rewrite fol_sem_congruence. split; [ | msplit 2 ]. + split. * intros s _ v w H; rewrite HE. f_equal; apply vec_pos_ext; intros p. apply HE, H. * intros r _ v w H. apply fol_equiv_ext; f_equal. apply vec_pos_ext; intros p. apply HE, H. + intros ?; rewrite HE; auto. + intros ? ? ?; rewrite !HE; intros; subst; auto. + intros ? ?; rewrite !HE; intros; subst; auto. Qed.
imports: List Arith Lia Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops fo_sig fo_terms fo_logic fo_congruence fo_sat)