PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
rel
1
1
wf
A
,
B
:Type,
R
:(
A
B
Prop). (
R
is 1-1)
Type
By:
Compute
Co
R
is 1-1 *
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
BProp). (R is 1-1) 
Type A,B:Type, R:(ABProp). (R is 1-1) Type
x,x':A, y,y':B. R(x,y) & R(x',y') 
(x = x' A 
y = y' B)
