fact: Record chain (n:nat) := { f :> nat -> D; chain_zero : f 0 = rho 0; chain_succ : forall m, m < n -> ierel (f m) (f 0) (f (S m)) (f 0) }.
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