proposition: Theorem Σsyms_Σnosyms_complete : @fo_form_fin_dec_eq_SAT_in (Σnosyms Σ) e eq_refl (Σsyms_Σnosyms ls A) X -> fo_form_fin_discr_dec_SAT_in A X.
proof: Proof. Proof using Hls HAls. intros (M & H1 & H2 & H3 & phi & H5). cbn in H3. exists. { intros x y. generalize (H2 e (x##y##ø)). intros []; [ left | right ]; try red; rewrite <- H3; auto. } exists (Σsyms_Σnosyms_rev_model H1 H2 H3 H5). exists H1. exists. { intros r v; simpl; apply H2. } exists phi. apply Σsyms_Σnosyms_complete_nested. 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 fol_ops fo_sig utils fo_terms fo_logic fo_sat) Undecidability.Shared.ListAutomation