WhoCites
Definitions
MarkB
generic
Sections
NuprlLIB
Doc
Who Cites rel
inverse?
rel_inverse
Def R^-1(x,y) == y R x
Thm*
T1,T2:Type, R:(T1
T2
Prop). R^-1
T2
T1
Prop
Syntax:
R^-1
has structure:
rel_inverse(R)
About:
WhoCites
Definitions
MarkB
generic
Sections
NuprlLIB
Doc
T1,T2:Type, R:(T1
T2Prop). R^-1 
T2T1PropT1,T2:Type, R:(T1T2Prop). R^-1 T2T1Prop
