proposition: Lemma sp_eval_ext s s' E : (forall n, s n = s' n) -> sp_eval s E = sp_eval s' E.
proof: Proof. intros HS. destruct E as [x|]; cbn; auto. 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