proposition: Lemma specialize_n_resolve n f2 a : specialize_n n f2 a = if Dec (a < n) then $(f2 a) else $(a-n).
proof: Proof. induction n as [|n IH] in f2,a|-*. - cbn. var_eq. - cbn. destruct a as [|a]. + easy. + cbn. unfold funcomp in IH. cbn in IH. rewrite IH. do 2 destruct (Dec _). 2,3: exfalso;lia. all:var_eq. 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)