(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
reverse
wf
1
1.
A
: Type
e
:Sexpr(
A
). Reverse(
e
)
Sexpr(
A
)
By:
AbRecTypeInd Concl
Generated subgoal:
1
2.
Q
: Sexpr(
A
)
Prop
3.
e
:{
e
:Sexpr(
A
)|
Q
(
e
) }. Reverse(
e
)
Sexpr(
A
)
4.
e
: ({
e
:Sexpr(
A
)|
Q
(
e
) }
{
e
:Sexpr(
A
)|
Q
(
e
) })+
A
Reverse(
e
)
Sexpr(
A
)
5
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
NuprlPrimitives
Sections
NuprlLIB
Doc
e:Sexpr(A). Reverse(e) 
Sexpr(A) e:Sexpr(A). Reverse(e) Sexpr(A)
Prop
e:{e:Sexpr(A)| Q(e) }. Reverse(e) Sexpr(A)
{e:Sexpr(A)| Q(e) })+A
Reverse(e) Sexpr(A)
