1. A : Type
2. B : AType
3. p : x:AB(x)
4. C : Type
5. D : Type
6. f : CD
7. b : x:AB(x)C
  f(p/x,y. b(x,y)) = (p/x,y. f(b(x,y)))

1

3. x : A 4. y : B(x) 5. C : Type 6. D : Type 7. f : CD 8. b : x:AB(x)C   f(b(x,y)) = f(b(x,y))

Auto

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