f:(D:Type. D(D List)), A:Type, a:A, B:Type, b:B. ||f(a)|| = ||f(b)||  

1

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

4 steps

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