(5steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
injtype
vs
inj
A
,
B
:Type. (
(
A
inj
B
))
(
f
:(
A
B
). Inj(
A
;
B
;
f
))
By:
Def of
A
inj
B
THEN UnivCD
Generated subgoal:
1
1.
A
: Type
2.
B
: Type
(
{
f
:(
A
B
)| Inj(
A
;
B
;
f
) })
(
f
:(
A
B
). Inj(
A
;
B
;
f
))
4
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
A,B:Type. (
(A inj
B)) 
(f:(A
B). Inj(A; B; f)) A,B:Type. ((A inj B)) (f:(AB). Inj(A; B; f)) B THEN UnivCD ({f:(AB)| Inj(A; B; f) }) (f:(AB). Inj(A; B; f))
