proposition: Lemma HFN_model' : forall x, ~ (hfs_inductive x).
proof: Proof. intros X HX. destruct (hfs_mem_fin_t X) as [L HL]. enough (S (length L) <= length L) by lia. rewrite <- list_numerals_length. apply NoDup_incl_length. - apply list_numerals_nodup. - intros x Hx. eapply HL, list_numerals_inductive, Hx. apply HX. 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