proposition: Lemma numeral_wf n : ~ numeral n ∈ numeral n.
proof: Proof. Proof using M_FST VIEQ. induction n. - apply M_eset. - intros [H|H] % sigma_el; fold numeral in *. + apply IHn. eapply numeral_trans; eauto. apply sigma_eq. + assert (numeral n ∈ numeral (S n)) by apply sigma_eq. now rewrite H in H0. 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)