Proofgold Proposition

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

type
prop

theory
HotG

name
lam_eta

proof
PUdQg..

Megalodon
lam_eta

proofgold address
TMMRn..^lam_eta

creator
4899 Pr6Pc../c09b5..

owner
4899 Pr6Pc../c09b5..

term root
19cd9..