Nuprl - Proof: dec iff ex bvfun 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: dec iff ex bvfun 2 1

1. T : Type
2. E : T

Prop
3. f : T

x,y:T. f(x,y)

E(x,y)
5. x : T
6. y : T

Dec(E(x,y))

By:	RWO "4<" 0

Generated subgoal:

1 Dec(f(x,y))
Auto

About:

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