proposition: Theorem Σ2_ΣSSn1_enc_sound : fo_form_fin_dec_SAT (Σ2_ΣSSn1_enc n A).
proof: Proof. Proof using HX M2_dec HA. exists Y, MSSn1. exists. { unfold Y; auto. } exists. { intros []; simpl; intros v. vec split v with x; vec nil v; clear v; simpl. destruct x as [ [ [] | x ] | (x1,x2) ]; try tauto. apply M2_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)