proposition: Lemma bounded_FV_term t n : bounded_t n t -> FV_term t < n.
proof: Proof. induction 1; try destruct f; cbn. assumption. 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 Undecidability.Synthetic.Definitions