1. f : D:Type. D(D List)
2. A : Type
3. a : A
4. B : Type
5. b : B
  ||f(a)|| = ||f(b)||  

By:	Use:[ | f(x):= ||f(x)|| | A | a | B | b] Inst: Thm* f:(D:Type. DT), A:Type, a:A, B:Type, b:B. f(a) = f(b)  T

1

(x.||f(x)||)  (D:Type. D)

3 steps

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html