proposition: Lemma pos_inj L d e : d el L -> e el L -> pos L d = pos L e -> d = e.
proof: Proof. induction L; cbn; try tauto. intros [->|Hd] [->|He]. all: repeat destruct Dec; try tauto; try congruence. intros [=]. auto. 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