(7steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
not
nat
occ
natfuns
1
1. (
) ~
False
By:
FwdThru:
Thm*
(
f
:(
A
B
). Bij(
A
;
B
;
f
))
(
B
~
A
) on [ (
) ~
]
THEN
Analyze-1
Generated subgoal:
1
2.
f
:
3. Bij(
;
;
f
)
False
5
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
) ~
False) ~
False
f:(AB). Bij(A; B; f)) 
(B ~ A) on [ () ~ ]
; ; f)
False
