(2steps total)
PrintForm
Definitions
mb
event
system
2
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
eqof
eq
btrue
A
:Type,
d
:EqDecider(
A
),
i
:
A
. (eqof(
d
)(
i
,
i
)) ~ true
By:
Auto THEN Analyze -2 THEN InstHyp [
i
;
i
] -2 THEN Unfold `eqof` 0 THEN Reduce 0
Generated subgoal:
1
1.
A
: Type
2.
eq
:
A
A
3.
x
,
y
:
A
.
x
=
y
eq
(
x
,
y
)
4.
i
:
A
5.
i
=
i
eq
(
i
,
i
)
(
eq
(
i
,
i
)) ~ true
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
mb
event
system
2
Sections
EventSystems
Doc
A:Type, d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true
A:Type, d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true
A
x,y:A. x = y 
eq(x,y)
eq(i,i)
(eq(i,i)) ~ true
