proposition: Lemma enc_point_inj d e : enc_point d = enc_point e -> d = e.
proof: Proof. Proof using LD_ex. apply pos_inj; apply LD_ex. 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