proposition: Lemma numeral_trans_sub x n : (forall x y, (x ∈ y) + (~ x ∈ y)) -> x ⊆ numeral n -> trans x -> sig (fun n => x = numeral n).
proof: Proof. Proof using M_FST VIEQ. intros d. induction n; cbn. - intros H _. exists 0. cbn. apply M_ext; trivial. intros y [] % M_eset. - intros Hn Hx. destruct (d (numeral n) x) as [H|H]. + exists (S n). cbn. apply M_ext; trivial. intros y [Hy| ->] % sigma_el; trivial. now apply (Hx (numeral n)). + apply IHn; trivial. intros y Hy. specialize (Hn y Hy). apply sigma_el in Hn as [Hn| ->]; tauto. 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)