fact: Definition is_inductive (t : term) := (∃ is_eset $0 ∧ $0 ∈ t`[↑]) ∧ ∀ $0 ∈ t`[↑] → (∃ is_sigma $1 $0 ∧ $0 ∈ shift 2 t).
imports: Undecidability.FOL.Utils.FullSyntax Undecidability.FOL.Sets.Signatures Undecidability.FOL.Sets.ZF List