IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
map equal1211 1. T : Type
2. T' : Type
3. a : T List
4. f : TT' 5. g : TT' 6. i:. i<||a|| f(a[i]) = g(a[i])
7. i : 8. i<||a||
f(a[i]) = g(a[i])
By:
BackThruSomeHyp
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T'
i:
. i<||a|| 
f(a[i]) = g(a[i])
f(a[i]) = g(a[i])
