(2steps total)
Remark
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
card
fun
vs
nsub
exp
1
1.
a
:
2.
b
:
(
a
b
) ~
(
b
a
)
By:
BackThru:
Thm*
a
:
,
b
:(
a
). (
i
:
a
b
(
i
)) ~
(
i
:
a
.
b
(
i
))
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
Remark
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
(a
b) ~ (b
a)
(ab) ~ (ba)
a:, b:(a). (i:ab(i)) ~ (
i:a. b(i))
