Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 x4 . x0 ∈ x4 ⟶ x1 ∈ x4 ⟶ x2 ∈ x4 ⟶ x3 ∈ x4 ⟶ lam 4 (λ x5 . If_i (x5 = 0) x0 (If_i (x5 = 1) x1 (If_i (x5 = 2) x2 x3))) ∈ setexp x4 4

as obj
-

as prop
c23e3..^{tuple_4_in_A_4}

theory
HotG

stx
a7e8b..

address
TMUtk..^{tuple_4_in_A_4}