proposition: Lemma finNum_eq m (f1 f2 : finNum m) : {f1=f2}+{f1<>f2}.
proof: Proof. destruct f1 as [m1 Hm1], f2 as [m2 Hm2]. destruct (eq_nat_decide m1 m2) as [Heq|Hne]; rewrite eq_nat_is_eq in *. - subst. left. f_equal. apply le_unique. - right. 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