Nuprl - Proof: proddeq-property 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: proddeq-property 1

1. A : Type
2. B : Type
3. e1 : A

x,y:A. x = y

e1(x,y)
5. eq : B

x,y:B. x = y

eq(x,y)
7. p1 : A
8. p2 : B
9. q1 : A
10. q2 : B
11. <p1,p2> = <q1,q2>

p1 = q1

By:	ApFunToHypEquands `z' 1of(z) A -1 THEN Reduce -1 THEN Trivial

Generated subgoals:

None

About:

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