A:Type, B:(AType), p:(x:AB(x)), C:Type, b:(x:AB(x)C).
  (p/x,y. b(x,y)) = b(1of(p),2of(p))

1

1. A : Type 2. B : AType 3. p : x:AB(x) 4. C : Type 5. b : x:AB(x)C   (p/x,y. b(x,y)) = b(1of(p),2of(p))

2 steps

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