Proofgold Proposition

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

proofgold address
TMTjk..^{MetaCatHFSet_terminal}

creator
9568 PrCx1../c0206..

owner
9568 PrCx1../c0206..

term root
703b9..