(4steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
one
one
corr
fams
indep
if
one
one
corr
A
,
A'
,
B
,
B'
:Type. (
A
~
A'
)
(
B
~
B'
)
(
:
A
.
B
) ~ (
:
A'
.
B'
)
By:
Auto
Generated subgoal:
1
1.
A
: Type
2.
A'
: Type
3.
B
: Type
4.
B'
: Type
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
DiscreteMath
Sections
DiscrMathExt
Doc
A,A',B,B':Type. (A ~ A') 
(B ~ B') 
