Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 . x3 ∈ setexp x1 x0 ⟶ ∀ x4 . x4 ∈ setexp x2 x1 ⟶ lam_comp x0 x4 x3 ∈ setexp x2 x0

as obj
-

as prop
4fede..^{lam_comp_exp_In}

theory
HotG

stx
6b5ba..

address
TMGg1..^{lam_comp_exp_In}