proposition: Lemma IB_F_succ_left rho : rho_canon rho -> rho ⊨ F_succ_left.
proof: Proof. intros H0. unfold F_succ_left. intros n [m Hnm]%(IB_N_e (n:=n)). 2:easy. exists (Pair m 0), (Num (S m)), (Pair (S m) 0). cbn. split. 2:lia. split. - eapply IB_P_i; cbn; try reflexivity. 1: congruence. apply H0. - eapply IB_P_i; cbn; try reflexivity. apply H0. 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