proposition: Lemma enc_point_pair d d1 d2 : enc_point d <> enc_pair d1 d2.
proof: Proof. unfold enc_pair. assert (H : enc_point d < S (length LD)) by apply pos_bound. lia. 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