proposition: Lemma finNum_fin m : cListable (finNum m).
proof: Proof. induction m as [|m [l IHl]]. - exists ((fN le0)::nil). intros [n u]. assert (n=0) as -> by lia. left. f_equal. apply le_unique. - exists ((fN le0)::map (fun k => match k with @fN _ n u => fN (leS u) end) l). intros [[|n] u]. + left. f_equal. apply le_unique. + right. rewrite in_map_iff. assert (n <= m) as Hu by lia. exists (fN Hu). split. * f_equal. apply le_unique. * apply IHl. Qed.
imports: Vector Undecidability.DiophantineConstraints(H10C Util.H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FullNDFacts Semantics.Tarski.FullSoundness Semantics.Tarski.FullFacts Syntax.BinSig Semantics.FiniteTarski.Full) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Undecidability.Shared.Libs.DLW.Wf(wf_finite) Coq(Arith Lia List) Undecidability.FOL.Semantics.FiniteTarski(Full DoubleNegation) Undecidability.Synthetic(Definitions DecidabilityFacts) Undecidability.Synthetic.Definitions Datatypes Relation_Definitions Setoid Relation_Definitions