(6steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
comp
preserves
surj
1
1.
A
: Type
2.
B
: Type
3.
C
: Type
4.
g
:
A
B
5.
f
:
B
C
6.
b
:
B
.
a
:
A
.
g
(
a
) =
b
7.
c
:
C
.
b
:
B
.
f
(
b
) =
c
8.
c
:
C
a
:
A
. (
f
o
g
)(
a
) =
c
By:
Reduce Concl
Generated subgoal:
1
a
:
A
.
f
(
g
(
a
)) =
c
4
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
B
b:B. 
a:A. g(a) = b
