Proofgold Proposition

∀ x0 : ο . (∀ x1 . (∀ x2 : ο . (∀ x3 : ι → ι . MetaCat_terminal_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_terminal

proofgold address
TMc3q..^{MetaCatSmallSet_terminal}

creator
9568 PrCx1../519a9..

owner
9568 PrCx1../519a9..

term root
1f793..