Nuprl - Proof: card sigma st dom

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card sigma st dom

A:Type, B:(A

Type), P:(A

Prop).

(i:{i:A| P(i) }

B(i)) ~ {v:(i:A

B(i))| P(v/x,y. x) }

By:	Guarding (<type> ~ <type>) SimilarTo: Thm* B:(AType), P:(AProp). Thm* (i:{i:A\| P(i) }B(i)) =ext {v:(i:AB(i))\| P(v/x,y. x) } THEN OOCifExteq

Generated subgoals:

None

About:

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