proposition: Lemma chain_data_unique (h:nat) (c1 c2 : chain h) : (forall k, k <= h -> chainData c1 k = chainData c2 k) -> c1 = c2.
proof: Proof. intros Heq. induction c1 as [|h n pl pr cc IHcc]. - refine (match c2 with chainZ => _ end). easy. - destruct (chain_inversion c2) as [[[[n' pl'] ph'] cc'] ->]. pose proof (Heq (S h) ltac:(lia)) as Heqh. cbn [chainData] in Heqh. destruct (Dec (S h = S h)) as [_|Hf]; [idtac|lia]. rewrite (IHcc cc'). + congruence. + intros k Hk. specialize (Heq k ltac:(lia)). cbn [chainData] in Heq. destruct (Dec (S h = k)) as [Ht|Hf]; [lia|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)