proposition: Lemma numeral_inj k l : numeral k = numeral l -> k = l.
proof: Proof. Proof using M_FST VIEQ. intros Hk. assert (k = l \/ k < l \/ l < k) as [H|[H|H]] by lia; trivial. all: apply numeral_lt in H; rewrite Hk in H; now apply numeral_wf in H. Qed.
imports: Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts FST) Undecidability.FOL(Sets.FST) Undecidability.FOL.TRAKHTENBROT(hfs) Undecidability.Shared.Libs.DLW.Utils(finite) Undecidability(Shared.ListAutomation) Coq(Lia)