Nuprl - Proof: card sigma distr 1 1

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

1. A : Type
2. B : A

Type
3. C : (x:A

B(x))

Type

(

xyz.xyz/xy,z. xy/x,y. <x,y,z>)

(xy:(x:A

B(x))

C(xy))

(x:A

y:B(x)

C(<x,y>))

By:	Analyze THEN New:[xy \| z] Analyze4 THEN New:[x \| y] Analyze4 THEN Reduce Concl

Generated subgoal:

1 4. x : A
5. y : B(x)
6. z : C(<x,y>)
<x,y,z> x:Ay:B(x)C(<x,y>)
Auto

About:

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