(8steps total)
PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
preserved
by
star
1
1.
T
: Type
2.
P
:
T
Prop
3.
R
:
T
T
Prop
4.
x
,
y
:
T
.
P
(
x
)
(
x
R
y
)
P
(
y
)
5.
x
:
T
6.
y
:
T
7.
P
(
x
)
8.
x
(
R
^*)
y
P
(
y
)
By:
Unfold `rel_star` -1 THEN Reduce -1 THEN ExRepD
Generated subgoal:
1
8.
n
:
9.
x
R
^
n
y
P
(
y
)
6
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(8steps total)
PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc
Prop
x,y:T. P(x) 
(x R y) 
P(y)
