proposition: Theorem reduction : MSLSAT ⪯ SLSAT.
proof: Proof. exists embed. intros P. split; intros (s & h & H1 & H2); exists s, h; split; trivial; now apply embed_sat. Qed.
imports: Undecidability.SeparationLogic(MSL SL) List Undecidability.Synthetic.Definitions