(4steps total)
PrintForm
Definitions
Lemmas
mb
nat
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
rel
star
symmetric
T
:Type,
R
:(
T
T
Prop). (Sym
x
,
y
:
T
.
x
R
y
)
(Sym
x
,
y
:
T
.
x
(
R
^*)
y
)
By:
Unfold `sym` 0 THEN Reduce 0
Generated subgoal:
1
1.
T
: Type
2.
R
:
T
T
Prop
3.
a
,
b
:
T
. (
a
R
b
)
(
b
R
a
)
4.
a
:
T
5.
b
:
T
6.
a
(
R
^*)
b
b
(
R
^*)
a
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
Lemmas
mb
nat
Sections
MarkB
generic
Doc
T:Type, R:(T
T
(Sym x,y:T. x (R^*) y)
