Proofgold Proposition

∀ 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

type
prop

theory
HotG

name
lam_comp_assoc

proof
PUXQg..

Megalodon
lam_comp_assoc

proofgold address
TMX7H..^{lam_comp_assoc}

creator
5919 Pr6Pc../05d1a..

owner
5919 Pr6Pc../05d1a..

term root
10d3c..