(7steps total)
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa
doc
sexpr
case
thm
1
1
2
1.
A
: Type
2.
s
: rec(
T
.(
T
T
)+
A
)
3.
y
:
A
4.
s
= inr(
y
)
(
x
:
A
. Inj(
y
) = Inj(
x
))
(
s1
,
s2
:Sexpr(
A
). Inj(
y
) = Cons(
s1
;
s2
))
By:
Select: 1
Generated subgoal:
1
x
:
A
. Inj(
y
) = Inj(
x
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
T)+A)
(
x:A. Inj(y) = Inj(x)) 
(
