proposition: Lemma IB_fulfills rho : rho ⊨ F -> H10UPC_SAT h10.
proof: Proof. intros H. unfold F in H. pose (Num 0 .: rho) as nrho. assert (rho_canon nrho) as nrho_canon. 1: split; easy. apply (@IB_aux_transport nrho), H; fold sat. - easy. - now apply IB_F_zero. - now apply IB_F_succ_left. - now apply IB_F_succ_right. 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