IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
card union swap11 1. A : Type
2. B : Type
InvFuns(A+B;B+A InvFuns;e.InjCase(e; x. inr(x); y. inl(y))
InvFuns;e.InjCase(e; x. inr(x); y. inl(y)))
By:
Analyze THEN Analyze-1 THEN Reduce Concl
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html