A:Type, B:(AType), f:x:A fp-> B(x).
  fpf-is-empty(f)  f =   x:A fp-> B(x)

By:	Auto THEN DVar `f' THEN All (i.Unfolds [`fpf`;`fpf-empty`;`fpf-is-empty`] i THEN Reduce i) THEN Try (Complete Auto)

1	1. A : Type 2. B : AType 3. d : A List 4. f1 : x:{x:A| (x  d) }B(x) 5. ||d||=0   <d,f1> = <nil,x.>  d:A Listx:{x:A| (x  d) }B(x)	2 steps
2	1. A : Type 2. B : AType 3. d : A List 4. f1 : x:{x:A| (x  d) }B(x) 5. <d,f1> = <nil,x.>  d:A Listx:{x:A| (x  d) }B(x)   ||d||=0	1 step

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