proposition: Lemma F_closed n : bounded n F.
proof: Proof. solve_bounds. apply emplace_exists_bounded. assert (forall k, k >= highest_var_list h10 -> bounded (k + S (S (S n))) (translate_list (S k) h10)) as Hk. 2: apply Hk; lia. intros k Hk. induction h10 as [|((xa &xb)& xc & xd) h10l IH] in Hk|-*. - cbn. solve_bounds. - cbn. cbn in Hk. solve_bounds. apply IH. lia. Qed.
imports: Vector Undecidability.DiophantineConstraints(H10C Util.H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FullNDFacts Semantics.Tarski.FullSoundness Semantics.Tarski.FullFacts Syntax.BinSig Semantics.FiniteTarski.Full) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Undecidability.Shared.Libs.DLW.Wf(wf_finite) Coq(Arith Lia List) Undecidability.FOL.Semantics.FiniteTarski(Full DoubleNegation) Undecidability.Synthetic(Definitions DecidabilityFacts) Undecidability.Synthetic.Definitions Datatypes Relation_Definitions Setoid Relation_Definitions