Proofgold Term Root Disambiguation

∀ x0 x1 : ι → (ι → ο) → ο . ∀ x2 . ∀ x3 x4 : ι → ο . ordinal x2 ⟶ TransSet x2 ⟶ (∀ x5 . x5 ∈ x2 ⟶ ∀ x6 : ι → ο . not (PNo_strict_imv x0 x1 x5 x6)) ⟶ PNo_strict_lowerbd x1 x2 x3 ⟶ PNo_strict_upperbd x0 x2 x4 ⟶ PNo_strict_lowerbd x1 x2 x4 ⟶ (∀ x5 . ordinal x5 ⟶ x5 ∈ x2 ⟶ iff (x3 x5) (x4 x5)) ⟶ ∀ x5 . x5 ∈ x2 ⟶ iff (x3 x5) (x4 x5)

as obj
-

as prop
d71fb..^{Conj_PNo_strict_imv_pred_eq__6__3}

theory
HotG

stx
202df..

address
TMS9C..^{Conj_PNo_strict_imv_pred_eq__6__3}