WhoCites
Definitions
mb
nat
Sections
MarkB
generic
Search
Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites rel
or?
rel_or
Def (
R1
R2
)(
x
,
y
) == (
x
R1
y
)
(
x
R2
y
)
Thm*
T
:Type,
R1
,
R2
:(
T
T
Prop). (
R1
R2
)
T
T
Prop
Syntax:
R1
R2
has structure:
rel_or(
R1
;
R2
)
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
mb
nat
Sections
MarkB
generic
Search
Doc
R2)(x,y) == (x R1 y) (x R2 y)
T:Type, R1,R2:(T
TProp). (R1 R2) 
TTProp R2)(x,y) == (x R1 y) (x R2 y)T:Type, R1,R2:(TTProp). (R1 R2) TTProp R2
