1. A : Type
2. P : AProp
3. x:A. Dec(P(x))
  f:(A). x:A. P(x)  f(x)

By:	Inst: Thm* Q:(ABProp). (x:A. y:B. Q(x,y))  (f:(AB). x:A. Q(x,f(x))) Using:[B:=  | Q(x,b):= P(x)  b]

1

4. x : A   y:. P(x)  y

1 step

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