Proofgold Proposition

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

type
prop

theory
HotG

name
lam_comp_id_R

proof
PUXQg..

Megalodon
lam_comp_id_R

proofgold address
TMPrb..^{lam_comp_id_R}

creator
5919 Pr6Pc../a6532..

owner
5919 Pr6Pc../a6532..

term root
0acec..