proposition: Lemma model_dec (h : heap) : decidable (fun v => i_atom (interp:=model h) (P:=tt) v).
proof: Proof. apply decidable_iff. constructor. intros v. cbn. apply pairlist_dec; exact _. 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