PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
flip
symmetry
k
:
,
i
,
j
:
k
. (
i
,
j
) = (
j
,
i
)
By:
Auto THEN Ext THEN Unfold `flip` 0 THEN Reduce 0 THEN Repeat SplitOnConclITE
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc