(2steps total)
PrintForm
Definitions
mb
event
system
5
Sections
EventSystems
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fpf-sub
weakening
A
:Type,
B
:(
A
Type),
eq
:EqDecider(
A
),
f
,
g
:
a
:
A
fp->
B
(
a
).
f
=
g
f
g
By:
Auto THEN HypSubst -1 0 THEN All Thin
Generated subgoal:
1
1.
A
: Type
2.
B
:
A
Type
3.
eq
: EqDecider(
A
)
4.
g
:
a
:
A
fp->
B
(
a
)
g
g
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
mb
event
system
5
Sections
EventSystems
Doc
A:Type, B:(A
Type), eq:EqDecider(A), f,g:a:A fp-> B(a). f = g 
f 
g
