Nuprl - Proof: assert-fpf-is-empty 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: assert-fpf-is-empty 1 1

1. A : Type
2. B : A

Type
3. d : A List
4. f1 : x:{x:A| (x

d) }

B(x)
5. d = nil

f1 = (

)

By:	Ext THEN Reduce 0 THEN Assert False THEN DVar `x' THEN Assert (x nil) THEN Subst (nil = d) 0 THEN Unfold `l_member` -1 THEN Reduce -1 THEN ExRepD

Generated subgoals:

None

About:

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