(3steps total) PrintForm core StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fun thru spread
  A:Type, B:(AType), p:(x:AB(x)), C,D:Type, f:(CD), b:(x:AB(x)C).
  f(p/x,y. b(x,y)) = (p/x,y. f(b(x,y)))
By: UnivCD

Generated subgoal:

1 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)))
2 steps

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

(3steps total) PrintForm core StandardLIB Doc