(2steps total)
PrintForm
Definitions
mb
event
system
1
Sections
EventSystems
Search
Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
l
member
subtype
A
,
B
:Type,
L
:
A
List,
x
:
A
. (
A
r
B
)
(
x
L
)
(
x
L
)
By:
Auto THEN RepeatFor 3 (ParallelOp -1) THEN RevHypSubst -1 0
Generated subgoal:
1
1.
A
: Type
2.
B
: Type
3.
L
:
A
List
4.
x
:
A
5.
A
r
B
6.
i
:
7.
x
=
L
[
i
]
x
=
x
B
1
step
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
mb
event
system
1
Sections
EventSystems
Search
Doc
A,B:Type, L:A List, x:A. (A 
r B) 
(x 
L) 
