IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
cons one one3 1. T : Type
2. a : T 3. a' : T 4. b : T List
5. b' : T List
6. a = a' 7. b = b' [a / b] = [a' / b']
By:
Obvious
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
[a / b] = [a' / b']
