(13steps total) PrintForm Definitions Lemmas mb event system 4 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fpf-all-single-decl 1 1
1. A : Type
2. eq : EqDecider(A)
3. B : AType
4. P : x:AB(x)Prop
5. x : A
6. v : B(x)
  (y:A. (eqof(eq)(x,y)  false)  P(y,v))  P(x,v)
By: Auto

Generated subgoals:

1 7. y:A. (eqof(eq)(x,y)  false)  P(y,v)
  P(x,v)
1 step
2 6. v : B(x)
7. y : A
8. eqof(eq)(x,y)  false
  v  B(y)
4 steps
3 7. P(x,v)
8. y : A
9. eqof(eq)(x,y)  false
  P(y,v)
4 steps

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

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