proposition: Lemma myenv_desc i : i <= highest_var_list h10 -> exists (H:rho i <= m), myenv i = Num (fN H).
proof: Proof. intros H. unfold myenv, into_fin, m. pose proof (highest_num_descr rho _ _ H) as Hpr. assert (rho i <= S (highest_num rho (highest_var_list h10))) as HH2 by lia. exists HH2. destruct leq_dec as [Hl|Hr]. - f_equal. f_equal. apply le_unique. - exfalso. now apply Hr, HH2. 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