proposition: Fact fo_form_fin_dec_SAT_fin : fo_form_fin_dec_SAT -> fo_form_fin_SAT.
proof: Proof. intros (X & M & H & _ & ?); exists X, M, H; trivial. Qed.
imports: List Undecidability.Shared.Libs.DLW.Utils(finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils decidable fol_ops fo_sig fo_terms fo_logic)