Proofgold Proposition

∀ x0 : ι → ο . x0 1 ⟶ x0 omega ⟶ MetaCat_nno_p x0 HomSet lam_id (λ x1 x2 x3 . lam_comp x1) 1 (λ x1 . lam x1 (λ x2 . 0)) omega (lam 1 (λ x1 . 0)) (lam omega ordsucc) (λ x1 x2 x3 . lam omega (nat_primrec (ap x2 0) (λ x4 . ap x3)))

type
prop

theory
HotG

name
-

proof
PUcag..

Megalodon
MetaCatSet_nno_gen

proofgold address
TMaB8..^{MetaCatSet_nno_gen}

creator
11547 PrEBh../17484..

owner
11561 PrEBh../ab4d5..

term root
b6c62..