Proofgold Term Root Disambiguation

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

as obj
-

as prop
64750..^{lam_comp_id_L}

theory
HotG

stx
6b5ba..

address
TMbj9..^{lam_comp_id_L}