Nuprl - Proof: trivial map 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: trivial map 1 1

1. T : Type
2. a : T List
3. f : T

T
4.

x:T. (x

f(x) = x
5. x : T
6. (x

f(x) = Id(x)

By:	Reduce 0 THEN EasyHyp

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html