Proofgold Object

SNo_rec2 (λ x0 x1 . λ x2 : ι → ι → ι . SNoCut (binunion {x2 x3 x1|x3 ∈ SNoL x0} (prim5 (SNoL x1) (x2 x0))) (binunion {x2 x3 x1|x3 ∈ SNoR x0} (prim5 (SNoR x1) (x2 x0))))

type
ι → ι → ι

theory
HotG

name
add_SNo

definition
PUK1b..

Megalodon
add_SNo

proofgold address
TMLfA..^add_SNo

creator
4949 Pr6Pc../81ce6..

owner
4949 Pr6Pc../81ce6..

term root
127d0..