proposition: Lemma IB_single_constr rho φ (n:nat) (h:h10upc) : rho_descr_phi rho φ n -> highest_var h < n -> rho ⊨ translate_single h (S n) -> h10upc_sem φ h.
proof: Proof. intros Hrhophi Hmaxhall. destruct h as [[a b][c d]]. unfold translate_single. cbn in Hmaxhall. intros (na&nb&nc&nd&Ha&Hb&Hc&Hd&Habcd)%IB_erel_e. unfold h10upc_sem. pose proof (Hrhophi a (ltac:(lia))) as Hpa. rewrite Ha in Hpa. pose proof (Hrhophi b (ltac:(lia))) as Hpb. rewrite Hb in Hpb. pose proof (Hrhophi c (ltac:(lia))) as Hpc. rewrite Hc in Hpc. pose proof (Hrhophi d (ltac:(lia))) as Hpd. rewrite Hd in Hpd. now rewrite <- Hpa, <- Hpb, <- Hpc, <- Hpd. 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