Proofgold Term Root Disambiguation

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

as obj
-

as prop
51ef7..^{lam_comp_assoc}

theory
HotG

stx
6b5ba..

address
TMGNE..^{lam_comp_assoc}