Proofgold Proposition

∀ x0 . ∀ x1 : ι → ι . SNo_recipaux x0 x1 0 = lam 2 (λ x3 . If_i (x3 = 0) (Sing 0) 0)

type
prop

theory
HotG

name
SNo_recipaux_0

proof
PUewm..

Megalodon
SNo_recipaux_0

proofgold address
TMUbG..^{SNo_recipaux_0}

creator
27779 PrQUS../d40bd..

owner
27779 PrQUS../d40bd..

term root
1a110..