proposition: Lemma hfs_numeral_inj n n' : hfs_numeral n = hfs_numeral n' -> n = n'.
proof: Proof. intros Hn. assert (n < n' \/ n = n' \/ n' < n) as [H|[H|H]] by lia; trivial. - apply hfs_numeral_lt in H. rewrite Hn in H. now apply hfs_no_loop in H. - apply hfs_numeral_lt in H. rewrite Hn in H. now apply hfs_no_loop in H. Qed.
imports: Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts) Undecidability.FOL(Sets.ZF) Undecidability.FOL(ZF) Undecidability.FOL.TRAKHTENBROT(hfs) Undecidability.Shared.Libs.DLW.Utils(finite) Undecidability(Shared.ListAutomation) Lia