proposition: Lemma chain_N n (c:chain n) m : m <= n -> iN (c m).
proof: Proof. Proof using HA1. intros Hm. destruct m. - rewrite (chain_zero c). apply HA1. - destruct (chain_succ c Hm) as [d1 [d0 [[_ H] _]]]. unfold iP in H. apply H. 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