mb
event
system
2
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
a
:Id.
a
=
a
~ true
[eq_id_self]
cites the following:
Thm*
d
:EqDecider(
A
),
i
:
A
. (eqof(
d
)(
i
,
i
)) ~ true
[eqof_eq_btrue]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
event
system
2
Sections
EventSystems
Doc
a:Id. a = a ~ true
d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ truea:Id. a = a ~ trued:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true