WhoCites Definitions mb nat Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites rel inverse?
rel_inverseDef R^-1(x,y) == y R x
Thm* T1,T2:Type, R:(T1T2Prop). R^-1  T2T1Prop

Syntax:R^-1 has structure: rel_inverse(R)

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

WhoCites Definitions mb nat Sections MarkB generic Doc