PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
rel
1
1
b
wf
A
,
B
:Type,
R
:(
A
B
Type). (1-1
x
A
,
y
B
.
R
(
x
;
y
))
Type
By:
Compute
Co
1-1
x
A
,
y
B
.
R
(
x
;
y
)
Co
*
Co
x
,
x'
:
A
,
y
,
y'
:
B
.
R
(
x
;
y
) &
R
(
x'
;
y'
)
(
x
=
x'
A
y
=
y'
B
)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
A,B:Type, R:(A
BType). (1-1 x
A,yB. R(x;y)) Type A,B:Type, R:(ABType). (1-1 xA,yB. R(x;y)) TypeA,yB. R(x;y)
x,x':A, y,y':B. R(x;y) & R(x';y') 
(x = x' A 
y = y' B)
