(4steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
finite
indep
sum
card
A
,
B
:Type,
a
,
b
:
. (
A
~
a
)
(
B
~
b
)
((
A
B
) ~
(
a
b
))
By:
Auto
Generated subgoal:
1
1.
A
: Type
2.
B
: Type
3.
a
:
4.
b
:
5.
A
~
a
6.
B
~
b
(
A
B
) ~
(
a
b
)
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
A,B:Type, a,b:
. (A ~ a) 
(B ~ b) ((A
B) ~ (a
b)) A,B:Type, a,b:. (A ~ a) (B ~ b) ((AB) ~ (ab))
a
b
(AB) ~ (ab)
