(4steps total) PrintForm Definitions mb event system 4 Sections EventSystems Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fpf-cap-single1
  A:Type, eq:EqDecider(A), x:A, v,z:Top. x : v(x)?z ~ v
By: UnivCD THEN Unfolds [`fpf-cap`;`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
2 steps
2 1. A : Type
2. eq : EqDecider(A)
3. x : A
4. v : Top
5. z : Top
  if true  false <[x],x.v>(x) else z fi ~ v
1 step

About:
pairconsnilboolbfalsebtrueifthenelse
lambdaapplyuniverseequalsqequaltopall
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

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