proposition: Lemma hfs_model_standard {x} : htrans x -> sig (fun n => x = numeral n).
proof: Proof. induction x using hfs_rect. intros Hx. destruct (hfs_mem_fin_t x) as [L HL]. unshelve edestruct (@max _ L) as [N HN]. - intros y Hy % HL. destruct (H y) as [n Hn]; auto. eapply htrans_htrans; eauto. - apply numeral_trans_sub with N. + apply hfs_model. + reflexivity. + intros a b. destruct (hfs_mem_dec a b); auto. + intros y Hy. destruct (H y Hy (htrans_htrans Hx Hy)) as [n Hn]. rewrite Hn. apply numeral_lt; try apply hfs_model; try reflexivity. assert (HLy : y el L) by now apply HL. specialize (HN y HLy). cbn in HN. destruct H as [n' ->] in HN. erewrite numeral_inj at 1; try apply HN; try apply hfs_model; try reflexivity. now rewrite Hn. + apply (proj1 Hx). 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)