1. A : Type
2. B : AType
3. Q : x:AB(x)Prop
4. x:A. y:B(x). Q(x,y)
  f:(x:AB(x)). x:A. Q(x,f(x))

By:	Compute4 x:A. y:B(x). Q(x,y) * x:Ay:B(x)Q(x,y) THEN Rename4: g THEN Witness z.1of(g(z)) THEN Compute (z.1of(g(z)))(x) * 1of(g(x))

1

4. g : x:Ay:B(x)Q(x,y) 5. x : A   Q(x,1of(g(x)))

4 steps

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