Proofgold Proposition

∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_u x1) ⟶ x0 (pack_u 1 (λ x1 . x1)) ⟶ MetaCat_terminal_p x0 UnaryFuncHom struct_id struct_comp (pack_u 1 (λ x1 . x1)) (λ x1 . lam (ap x1 0) (λ x2 . 0))

type
prop

theory
HotG

name
-

proof
PUYhi..

Megalodon
-

proofgold address
TMGWT..

creator
11768 PrEBh../50ddb..

owner
11768 PrEBh../50ddb..

term root
4c2c2..