proposition: Lemma hfs_numeral_lt n n' : n < n' -> hfs_mem (hfs_numeral n) (hfs_numeral n').
proof: Proof. induction n'; try lia. intros Hn. cbn. apply hfs_cons_spec. assert (n = n' \/ n < n') as [->|H] by lia; auto. 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