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)

By:	RW assert_pushdownC -1 THEN RWO Thm* l:T List. ||l|| = 0    l = nil -1 THEN Analyze THEN Try (Complete Auto)

1

5. d = nil   f1 = (x.)

1 step

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