proposition: Lemma model_fin m : cListable (model m).
proof: Proof. destruct (finNum_fin m) as [l Hl]. exists (map (@Num m) l ++ flat_map (fun v => map (Pair v) l) l). intros [n|a b]. - apply in_or_app. left. apply in_map, Hl. - apply in_or_app. right. rewrite in_flat_map. exists a. split. 1:apply Hl. apply in_map, Hl. 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