(11steps total)
Remark
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
simple
card
cross
assoc
A
,
B
,
C
:Type. (
A
B
C
) ~ ((
A
B
)
C
)
By:
UnivCD
Generated subgoal:
1
1.
A
: Type
2.
B
: Type
3.
C
: Type
(
A
B
C
) ~ ((
A
B
)
C
)
10
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(11steps total)
Remark
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
A,B,C:Type. (A
BC) ~ ((AB)C) A,B,C:Type. (ABC) ~ ((AB)C) (ABC) ~ ((AB)C)
