fact: Definition is_union (x t : term') := ∀ $0 ∈ t`[↑] <~> ∃ $0 ∈ shift 2 x ∧ $1 ∈ $0.
imports: Undecidability.FOL.Util.Syntax Undecidability.FOL.Util.FullTarski Undecidability.FOL.Util.FullDeduction Undecidability.FOL.ZF List