proposition: Fact Σ_finite_rev_correct A : fo_form_fin_dec_SAT A <-> fo_form_fin_dec_SAT (Σ_finite_rev A).
proof: Proof. split. + intros (X & M' & H1 & H2 & phi & H3). exists X, (Σ_finite_rev_model1 M' (phi 0)), H1. exists. { intros r v; simpl. destruct (in_dec HΣ2 r lr). + apply H2. + tauto. } exists phi. apply Σ_finite_rev_sound; auto. + intros (X & M & H1 & H2 & phi & H3). exists X, (Σ_finite_rev_model2 M), H1. exists. { intros (r & Hr) v; simpl; apply H2. } exists phi; apply Σ_finite_rev_complete; auto. 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)