Proofgold Proposition

∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_initial_p (λ x4 . x4 ∈ 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
MetaCatHFSet_initial

proofgold address
TMSYF..^{MetaCatHFSet_initial}

creator
9568 PrCx1../282eb..

owner
9568 PrCx1../282eb..

term root
0741f..