A:Type, B:(AType), Q:(x:AB(x)Type).
  (x:A. y:B(x). Q(x,y))  (f:(x:AB(x)). x:A. Q(x,f(x)))

1

1. A : Type 2. B : AType 3. Q : x:AB(x)Type 4. x:A. y:B(x). Q(x,y)   f:(x:AB(x)). x:A. Q(x,f(x))

6 steps

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