PrintForm
Definitions
mb
event
system
2
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
deq
property
T
:Type,
d
:EqDecider(
T
),
x
,
y
:
T
.
x
=
y
eqof(
d
)(
x
,
y
)
By:
Unfolds [`deq`;`eqof`] 0 THEN Analyze 2 THEN All Reduce THEN BackThru 3
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
mb
event
system
2
Sections
EventSystems
Doc
T:Type, d:EqDecider(T), x,y:T. x = y 
eqof(d)(x,y) T:Type, d:EqDecider(T), x,y:T. x = y eqof(d)(x,y)
