proposition: Theorem FSAT_in_ext Σ A X (P Q : X -> bool) : (forall x, P x = true <-> Q x = true) -> @fo_form_fin_dec_SAT_in Σ A (sig (fun x => P x = true)) <-> @fo_form_fin_dec_SAT_in Σ A (sig (fun x => Q x = true)).
proof: Proof. intros H; split. + intros (M & H1 & H2 & phi & H3). apply fo_form_fin_dec_SAT_in_ext with (M := M) (phi := phi); auto; intros; apply eq_bool_pirr. + intros (M & H1 & H2 & phi & H3). apply fo_form_fin_dec_SAT_in_ext with (M := M) (phi := phi); auto. 2-3: intros; apply eq_bool_pirr. intros; rewrite H; tauto. 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 utils fol_ops fo_sig fo_terms fo_logic fo_sat decidable)