(3steps 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-val-single1
  A:Type, eq:EqDecider(A), x:A, v,P:Top.
  z != x : v(x) ==> P(a,z) ~ (True  P(x,v))
By: UnivCD THEN Unfolds [`fpf-val`;`fpf-single`] 0 THEN Unfold `fpf-dom` 0
THEN
Reduce 0
THEN
Subst' (eqof(eq)(x,x) = true) 0

Generated subgoals:

1 1. A : Type
2. eq : EqDecider(A)
3. x : A
4. Top
5. Top
  eqof(eq)(x,x) = true
1 step
2 1. A : Type
2. eq : EqDecider(A)
3. x : A
4. v : Top
5. P : Top
  ((true  false)  P(x,<[x],x.v>(x))) ~ (True  P(x,v))
1 step

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

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