Proofgold Proposition

∀ x0 x1 x2 x3 . x3 ∈ setexp x1 x0 ⟶ ∀ x4 . x4 ∈ setexp x2 x1 ⟶ lam_comp x0 x4 x3 ∈ setexp x2 x0

type
prop

theory
HotG

name
lam_comp_exp_In

proof
PUXQg..

Megalodon
lam_comp_exp_In

proofgold address
TMHzP..^{lam_comp_exp_In}

creator
5919 Pr6Pc../6d396..

owner
5919 Pr6Pc../6d396..

term root
a368c..