A:Type, B:(AType), C:((x:AB(x))Type).
  (xy:(x:AB(x))C(xy)) ~ (x:Ay:B(x)C(<x,y>))

1

1. A : Type 2. B : AType 3. C : (x:AB(x))Type   (xy:(x:AB(x))C(xy)) ~ (x:Ay:B(x)C(<x,y>))

4 steps

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