proposition: Lemma m_discrete m : discrete (model m).
proof: Proof. assert (forall (d1 d2 : model m), {d1=d2}+{d1<>d2}) as Heq by (intros d1 d2; repeat decide equality; apply finNum_eq). eexists (fun '(a, b) => if Heq a b then true else false). intros [a b]. split; intros ?; destruct (Heq a b); congruence. Defined.
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