IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc type poly swap112 1. f : C,D:Type. CDDC 2. A : Type
3. B : Type
4. a : A 5. b : B 6. f {a:A}{b:B}{b:B}{a:A}
a {a:A}
By:
Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html