(2steps 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
cdr
wf
A
:Type,
s
:Sexpr(
A
). sexprCdr(
s
)
Sexpr(
A
)
By:
Def of sexprCdr(
s
)
Generated subgoal:
1
1.
A
: Type
2.
s
: Sexpr(
A
)
(Case of
s
: Inj(
x
)
Inj(
x
) ; Cons(
s1
;
s2
)
s2
)
Sexpr(
A
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
A:Type, s:Sexpr(A). sexprCdr(s) 
Sexpr(A) A:Type, s:Sexpr(A). sexprCdr(s) Sexpr(A) (Case of s : Inj(x) 
Inj(x) ; Cons(s1;s2) s2) Sexpr(A)
