Proofgold Proposition

∀ x0 : ι → ο . (∀ x1 . x0 x1 ⟶ struct_c x1) ⟶ MetaCat x0 PreContinuousHom (λ x1 . lam_id (ap x1 0)) (λ x1 x2 x3 . lam_comp (ap x1 0))

type
prop

theory
HotG

name
-

proof
PUdXV..

Megalodon
MetaCat_struct_c_gen

proofgold address
TMGrW..^{MetaCat_struct_c_gen}

creator
9630 PrCx1../67bb2..

owner
9630 PrCx1../67bb2..

term root
a1cc1..