proposition: Theorem reduction : FSATdc ⪯ MSLSAT.
proof: Proof. exists (fun phi => encode' (proj1_sig phi)). intros [phi H]; unfold FSATdc; cbn. apply reduction'. change nil with (seq 0 0). now apply bounded_FV. Qed.
imports: Undecidability.FOL(Semantics.FiniteTarski.Full) Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts Syntax.BinSig) Undecidability.SeparationLogic(MSL) Undecidability.Shared(Dec) Undecidability.Synthetic.DecidabilityFacts List Undecidability.Synthetic.Definitions