Proofgold Term Root Disambiguation

λ x0 x1 . x0 ∈ u17 ⟶ x1 ∈ u17 ⟶ bb6a5.. (u17_to_Church17 x0) (u17_to_Church17 x1) = λ x3 x4 . x3

as obj
e5bd5..

as prop
-

theory
HotG

stx
0f832..

address
TMRHL..