Proofgold Proposition

∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_r x1) ⟶ x0 (pack_r 1 (λ x1 x2 . True)) ⟶ MetaCat_terminal_p x0 BinRelnHom struct_id struct_comp (pack_r 1 (λ x1 x2 . True)) (λ x1 . lam (ap x1 0) (λ x2 . 0))

type
prop

theory
HotG

name
-

proof
PUSP5..

Megalodon
-

proofgold address
TMJrv..

creator
11866 PrEBh../a82ff..

owner
11866 PrEBh../a82ff..

term root
9fbd3..