PrintForm
Definitions
LogicSupplement
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
diagonalize
wf
B
:Type,
e
:(
B
B
),
A
:Type,
f
:(
A
A
B
). (Diag
f
wrt
y
.
e
(
y
))
A
B
By:
Def of Diag <fn> wrt [var]. <*>
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
LogicSupplement
Sections
DiscrMathExt
Doc
B:Type, e:(B
B), A:Type, f:(AAB). (Diag f wrt y. e(y)) 
AB B:Type, e:(BB), A:Type, f:(AAB). (Diag f wrt y. e(y)) AB
