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