(3steps 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
2
weakening
wrt
1
1.
A
: Type
2.
B
: Type
3.
A
=
B
f
:(
A
B
),
g
:(
B
A
). InvFuns(
A
;
B
;
f
;
g
)
By:
Subst
:
A
=
B
Type THEN Witness: Id | Id
Generated subgoal:
1
InvFuns(
A
;
A
;Id;Id)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
f:(A
B), g:(B
: A = B 
Type THEN Witness: Id | Id
