Proofgold Term Root Disambiguation

λ x0 x1 . PNoLe (SNoLev x0) (λ x2 . x2 ∈ x0) (SNoLev x1) (λ x2 . x2 ∈ x1)

as obj
54f40..^SNoLe

as prop
-

theory
HotG

stx
fab7c..

address
TMKo9..^SNoLe