Proofgold Proposition

∃ x0 . ∃ x2 : ι → ι . MetaCat_terminal_p (λ x4 . True) HomSet (λ x4 . lam x4 (λ x5 . x5)) (λ x4 x5 x6 x7 x8 . lam x4 (λ x9 . ap x7 (ap x8 x9))) x0 x2

type
prop

theory
HotG

name
-

proof
PUNFE..

Megalodon
MetaCatSet_terminal

proofgold address
TMLHA..^{MetaCatSet_terminal}

creator
9568 PrCx1../b4ee5..

owner
9568 PrCx1../b4ee5..

term root
bf778..