PrintForm
Definitions
Lemmas
mb
event
system
2
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
eq
id
self
a
:Id.
a
=
a
~ true
By:
Auto THEN Unfold `eq_id` 0
THEN
RWO
Thm*
d
:EqDecider(
A
),
i
:
A
. (eqof(
d
)(
i
,
i
)) ~ true
0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
mb
event
system
2
Sections
EventSystems
Doc
a:Id. a = a ~ true
a:Id. a = a ~ trued:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true 0
