proposition: Lemma pos_bound L x : pos L x < S (length L).
proof: Proof. induction L; cbn. - lia. - decide (x = a); 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