proposition: Lemma enc_pair_inj d d' e e' : enc_pair d d' = enc_pair e e' -> d = e /\ d' = e'.
proof: Proof. Proof using LD_ex. intros H. assert (((enc_point d), (enc_point d')) = ((enc_point e), (enc_point e'))) as [=]. - apply enc_npair_inj. unfold enc_pair in H. lia. - split; now apply enc_point_inj. 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