Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . nat_p x0∀ x1 . x1SNoS_ (ordsucc x0)SNoLt 0 x1SNoEq_ (SNoLev x1) (eps_ x0) x1∀ x2 : ο . (∀ x3 . and (x3x0) (x1 = eps_ x3)x2)x2
as obj
-
as prop
8515a..eps_SNo_eq
theory
HotG
stx
26642..
address
TMQ16..eps_SNo_eq