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. rewrite IB_Not. cbn. intros Hc. specialize (Hc (Pair m 0) (Num (S m)) (Pair (S m) 0)). eapply IB_P_e in Hc. 2-4:easy. 2: exists m, 0; cbn; auto. eapply IB_P_e in Hc. 2-4:easy. 2: exists (S m), 0; cbn; auto. rewrite IB_wFalse. unfold scons. cbn in Hc. rewrite IB_wFalse in Hc. unfold scons in Hc. apply Hc; split; lia. Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FragmentNDFacts Semantics.Tarski.FragmentSoundness Semantics.Tarski.FragmentFacts Syntax.BinSig Semantics.Kripke.FragmentCore Semantics.Kripke.FragmentSoundness Semantics.Kripke.FragmentToTarski) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Undecidability.Shared(ListAutomation) Coq(Arith Lia List)