proposition: Theorem reduction : FSATd ⪯ FSATdc.
proof: Proof. exists form2cform. intros phi; unfold FSATdc; cbn. unfold exclosure. destruct find_bounded as [N HN]. split; intros (D & M & rho & H1 & H2 & H3 & H4); exists D, M. - exists rho. repeat split; trivial. eapply subst_exist_sat; eauto. - apply subst_exist_sat2 in H4 as [sigma H]. exists sigma. repeat split; trivial. Qed.
imports: Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Semantics.FiniteTarski.Full) Undecidability.Synthetic.Definitions Vector Lia