proposition: Lemma dom_discrete h : discrete (dom h).
proof: Proof. apply discrete_iff. constructor. intros [x Hx] [y Hy]. decide (x = y) as [H|H]. - left. now apply dom_eq. - right. now intros [=]. 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