1. A : Type
2. eq : EqDecider(A)
3. P : ATypeProp
4. f : x:A fp-> Type
5. g : x:A fp-> Type
6. y:A. y  dom(f)  P(y,f(y))
7. y:A. y  dom(g)  P(y,g(y))
8. y : A
9. y  dom(f)  y  dom(g)
10. y  dom(f)
  y  dom(g)

None

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