Proofgold Proposition

∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_p x1) ⟶ x0 (pack_p 1 (λ x1 . True)) ⟶ MetaCat_terminal_p x0 UnaryPredHom struct_id struct_comp (pack_p 1 (λ x1 . True)) (λ x1 . lam (ap x1 0) (λ x2 . 0))

type
prop

theory
HotG

name
-

proof
PUSP5..

Megalodon
-

proofgold address
TMJj8..

creator
11866 PrEBh../84b83..

owner
11866 PrEBh../84b83..

term root
eaa5e..