(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 1
1. A : Type
2. eq : EqDecider(A)
3. x : A
4. Top
5. Top
  eqof(eq)(x,x) = true
By: RWO Thm* d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true 0

Generated subgoals:

None

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