proposition: Theorem Σfull_mon_rem_sound : fo_form_fin_dec_SAT_in Σfull_mon_red K.
proof: Proof. Proof using HwA Kfin Mdec HA. exists M', Kfin. exists. { intros [ (w,r) | r ]; simpl in r |- *; intro; apply Mdec. } exists φ; simpl; split. + apply Σfull_mon_rec_sound; auto. + intro x; rewrite fol_sem_lconj. intros ?; rewrite in_map_iff. intros ((([|s w]&Hw),r) & <- & Hr); unfold Eq. * simpl; auto. * simpl; 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 Sig_no_syms)