proposition: Theorem Σfull_mon_rem_complete : fo_form_fin_dec_SAT_in A K.
proof: Proof. Proof using HwA Kfin M'dec HA. exists M, Kfin. exists. { intros r'; simpl in r'; intros v; apply M'dec. } exists φ; simpl. simpl in HA. destruct HA as [ H1 H2 ]. revert H1; apply Σfull_mon_rec_complete. + intros s w r x Hw. simpl in H2; specialize (H2 x). rewrite fol_sem_lconj in H2. symmetry; apply (H2 (Eq (exist _ (s::w) Hw,r))), in_map_iff. exists (exist _ (s::w) Hw,r); split; auto. + intros r x. simpl in H2; specialize (H2 x). rewrite fol_sem_lconj in H2. symmetry; apply (H2 (Eq (exist _ nil (Nat.lt_0_succ _),r))), in_map_iff. exists (exist _ nil (Nat.lt_0_succ _),r); split; 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)