Proofgold Proposition

∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_initial_p (λ x4 . x4 ∈ prim6 (prim6 0)) HomSet (λ x4 . lam x4 (λ x5 . x5)) (λ x4 x5 x6 x7 x8 . lam x4 (λ x9 . ap x7 (ap x8 x9))) x1 x3 ⟶ x2) ⟶ x2) ⟶ x0) ⟶ x0

type
prop

theory
HotG

name
-

proof
PUNFE..

Megalodon
MetaCatSmallSet_initial

proofgold address
TMGgB..^{MetaCatSmallSet_initial}

creator
9568 PrCx1../5bb1b..

owner
9568 PrCx1../5bb1b..

term root
96463..