proposition: Lemma dom_eq h (x y : dom h) : proj1_sig x = proj1_sig y -> x = y.
proof: Proof. destruct x as [x Hx], y as [y Hy]; cbn. intros ->. f_equal. apply squash_pure. 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