Search for blocks/addresses/...

Proofgold Proposition

∀ x0 . SNo x0 ⟶ recip_SNo_pos x0 = SNoCut (famunion omega (λ x2 . ap (SNo_recipaux x0 recip_SNo_pos x2) 0)) (famunion omega (λ x2 . ap (SNo_recipaux x0 recip_SNo_pos x2) 1))
type
prop
theory
HotG
name
recip_SNo_pos_eq
proof
PUewm..
Megalodon
recip_SNo_pos_eq
proofgold address
TMJSV..recip_SNo_pos_eq
creator
27779 PrQUS../010e1..
owner
27779 PrQUS../010e1..
term root
2e3e0..