Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι . lam x0 (ap (lam x0 x1)) = lam x0 x1

as obj
-

as prop
9103b..^lam_eta

theory
HotG

stx
08e38..

address
TMTTD..^lam_eta