(4steps total) PrintForm Definitions mb event system 5 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fpf-compatible-singles
  A:Type, eq:EqDecider(A), B:(AType), x,y:A, v:B(x), u:B(y).
  (x = y  v = u  B(x))  x : v || y : u
By: Auto

Generated subgoals:

1 1. A : Type
2. eq : EqDecider(A)
3. B : AType
4. x : A
5. y : A
6. v : B(x)
7. u : B(y)
8. x = y  v = u  B(x)
  x : v || y : u
2 steps
2 1. A : Type
2. EqDecider(A)
3. B : AType
4. x : A
5. y : A
6. B(x)
7. u : B(y)
8. x = y
  u  B(x)
1 step

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

(4steps total) PrintForm Definitions mb event system 5 Sections EventSystems Doc