(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
1
1
1.
T
: Type
2.
E
:
T
T
Prop
3. EquivRel(
T
)(_1
E
_2)
x
,
y
:
T
. (
x
E
^0
y
)
(
x
E
y
)
By:
RecUnfold `rel_exp` 0 THEN Reduce 0
Generated subgoal:
1
4.
x
:
T
5.
y
:
T
6.
x
=
y
x
E
y
1
step
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
T
x,y:T. (x E^0 y) 
(x E y)
