(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
  A:Type{i'}, eq:EqDecider(A), B:(AType{i'}), P:(x:AB(x)Prop{i}), x:A,
  v:B(x). ydom(x : v). w=x : v(y)   P(y,w)  P(x,v)
By: UnivCD THEN Unfold `fpf-all` 0 THEN Unfolds [`fpf-dom`;`fpf-single`;`fpf-ap`] 0
THEN
Reduce 0

Generated subgoal:

1 1. A : Type{i'}
2. eq : EqDecider(A)
3. B : AType{i'}
4. P : x:AB(x)Prop{i}
5. x : A
6. v : B(x)
  (y:A. (eqof(eq)(x,y)  false)  P(y,v))  P(x,v)
10 steps

About:
bfalseassertapplyfunctionuniversepropimpliesall
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