proposition: Lemma chain_inversion n (c:chain n) : (match n return chain n -> Type with 0 => fun cc => cc = chainZ | S nn => fun cc' => {'(n,pl,ph,cc) & cc' = chainS n pl ph cc} end) c.
proof: Proof. destruct c as [|m n pl pr c]. 1:easy. exists (n,pl,pr,c). easy. 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)