proposition: Theorem Σ2_ΣSSn1_enc_complete : fo_form_fin_dec_SAT A.
proof: Proof. Proof using All. exists X, M2. exists. { unfold X; apply fin_t_finite_t. + intros; apply eq_bool_pirr. + unfold Q; apply finite_t_fin_t_dec; auto. intros; apply bool_dec. } exists. { intros [] v; simpl; apply MSSn1_dec. } exists φ; auto. 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)