Proofgold Term Root Disambiguation

∀ x0 x1 : ι → ι . ∀ x2 . nat_p x2 ⟶ (∀ x3 . x3 ∈ x2 ⟶ x0 x3 = x1 x3) ⟶ 05ecb.. x0 x2 = 05ecb.. x1 x2

as obj
-

as prop
9a5d6..^Pi_SNo_eq

theory
HotG

stx
afc5a..

address
TMb46..^Pi_SNo_eq