proposition: Lemma IB_translate_rec rho phi f e hv : rho_descr_phi rho phi hv -> highest_var_list e < hv -> rho ⊨ translate_rec f (S hv) e -> (forall c, In c e -> h10upc_sem phi c) /\ rho ⊨ f.
proof: Proof. intros Hrhophi Hhv H. induction e as [|eh er IH] in H,Hhv|-*. - split. 1: intros c []. easy. - cbn. cbn in H, Hhv. destruct IH as [IH1 IH2]. 1:lia. 1:apply H. split. 2:easy. intros c [->|Her]. + eapply (IB_single_constr Hrhophi). 1:lia. apply H. + now apply IH1. Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FullNDFacts Semantics.Tarski.FullSoundness Semantics.Tarski.FullFacts Syntax.BinSig) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Coq(Arith Lia List) Undecidability.Synthetic.Definitions