IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
flip inverse k:, x,y:k. (y, x) o (y, x) = (x.x)
By:
Auto THEN Ext THEN Unfold `flip` 0 THEN Reduce 0
THEN
Repeat (SplitOnConclITE THEN MoveToConcl -1)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
k:
, x,y:
k. (y, x) o (y, x) = (
x.x)
