Proofgold Term Root Disambiguation

∀ x0 . ∃ x1 . and (and (and (x0 ∈ x1) (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 . x4 ⊆ x3 ⟶ x4 ∈ x1)) (∀ x3 . x3 ∈ x1 ⟶ ∃ x4 . and (x4 ∈ x1) (∀ x6 . x6 ⊆ x3 ⟶ x6 ∈ x4))) (∀ x3 . x3 ⊆ x1 ⟶ or (∃ x4 : ι → ι . bij x3 x1 x4) (x3 ∈ x1))

as obj
-

as prop
4422b..

theory
HotG

stx
f4683..

address
TMZan..