(3steps total) PrintForm Definitions mb event system 2 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: proddeq-property
  A,B:Type, a:EqDecider(A), b:EqDecider(B), p,q:(AB).
  p = q  proddeq(a;b)(p,q)
By: UnivCD THEN Unfold `proddeq` 0 THEN Reduce 0 THEN Analyze 6 THEN Analyze 5
THEN
Analyze 4
THEN
Analyze 3
THEN
Reduce 0
THEN
RW assert_pushdownC 0
THEN
Try (Analyze THEN BackThruSomeHyp THEN Trivial)
THEN
Try BackThruSomeHyp

Generated subgoals:

1 1. A : Type
2. B : Type
3. e1 : AA
4. x,y:A. x = y  e1(x,y)
5. eq : BB
6. 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
1 step
2 1. A : Type
2. B : Type
3. e1 : AA
4. x,y:A. x = y  e1(x,y)
5. eq : BB
6. 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>
  p2 = q2
1 step

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

(3steps total) PrintForm Definitions mb event system 2 Sections EventSystems Doc