proposition: Lemma finsat_closed R : closed (finsat_formula R).
proof: Proof. unfold closed. solve_bounds. apply list_or_closed. intros a [x [<- Hx2]]%in_map_iff. solve_bounds. all: apply tprep_bounded; solve_bounds. Qed.
imports: Lia Arith Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.DecidabilityFacts Undecidability(FOL.Utils.FullSyntax) Undecidability(FOL.FSAT) Undecidability.Shared.ListAutomation