WhoCites Definitions mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites sym?
symDef Sym x,y:TE(x;y) == a,b:TE(a;b E(b;a)
Thm* T:Type, E:(TTProp). (Sym x,y:TE(x,y))  Prop

Syntax:Sym x,y:TE(x;y) has structure: sym(Tx,y.E(x;y))

About:
functionuniversememberpropimpliesall!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

WhoCites Definitions mb nat Sections MarkB generic Doc