IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
trivial map2 1. T : Type
2. a : T List
3. f : TT 4. x:T. (xa) f(x) = x 5. map(f;a) = map(Id;a)
map(f;a) = a
By:
HypSubst -1 0 THEN BackThru Thm*as:A List. map(Id;as) = as
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T
x:T. (x 
a) 
f(x) = x
map(f;a) = a
