Proofgold Term Root Disambiguation

∀ x0 x1 x2 . x2 ∈ setexp x1 x0 ⟶ lam_comp x0 x2 (lam_id x0) = x2

as obj
-

as prop
b8b0c..^{lam_comp_id_R}

theory
HotG

stx
6b5ba..

address
TMMEA..^{lam_comp_id_R}