proposition: Lemma enc_npair_inj n n' k k' : enc_npair n n' = enc_npair k k' -> (n, n') = (k, k').
proof: Proof. intros H. rewrite <- (decode_encode n n'), <- (decode_encode k k'). congruence. 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