Nuprl - Proof: all functionality wrt iff

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: all functionality wrt iff

S,T:Type, P,Q:(S

Prop).

S = T

(

x:S. P(x)

Q(x))

((

x:S. P(x))

(

y:T. Q(y)))

By:	GenUnivCD THEN HypBackchain

Generated subgoals:

None

About:

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