proposition: Lemma bounded_FV phi n : bounded n phi -> incl (FV phi) (seq 0 n).
proof: Proof. induction 1; cbn. - intros x [t [<- Ht]] % in_map_iff. apply to_list_in', H, bounded_FV_term in Ht. apply in_seq. lia. - auto using incl_app. - intros x [t [<- Ht]] % in_map_iff. apply filter_In in Ht as [H1 H2]. destruct t; try discriminate. apply IHbounded, in_seq in H1. cbn. apply in_seq. lia. - apply incl_nil_l. 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