Nuprl - Proof: subset exteq

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: subset exteq

A:Type, B,B':(A

Prop).

(

x:A. B(x)

B'(x))

({x:A| B(x) } =ext {x:A| B'(x) })

By:	Def of <type> =ext <type> THEN Repeat BackThruWithHyps: Thm* (x:A. B(x) B'(x)) {x:A\| B(x) } {x:A\| B'(x) }

Generated subgoals:

None

About:

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