(4steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
one
one
corr
fams
refl
1
2
1.
A
: Type
2.
B
:
A
Type
3.
u
:
A
InvFuns(
B
(
u
);
B
(
u
);Id;Id)
By:
BackThru:
Thm*
InvFuns(
A
;
A
;Id;Id)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
Type
InvFuns(B(u);B(u);Id;Id)
