Nuprl - Proof: pair eta rw 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: pair eta rw 1

1. A : Type
2. B : A

Type
3. p : a:A

B(a)

<1of(p),2of(p)> = p

a:A

B(a)

By:	Analyze 3 THEN AbReduce 0

Generated subgoal:

1 3. a : A
4. p1 : B(a)
<a,p1> = <a,p1> a:AB(a)
Auto

About:

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