WhoCites Definitions HOLlib Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites hrep sum?
hrep_sumDef rep_sum
Def == u:'a+'b. InjCase(u
Def == u:'a+'b. InjCasepb:x:'ay:'b. (x = p)b
Def == u:'a+'b. InjCaseqb:x:'ay:'b. (y = q)b)
Thm* 'a,'b:S. rep_sum  (hsum('a'b hbool  'a  'b  hbool)
bnotDef b == if b false else true fi
Thm* b:b  
bequalDef x = y == (x = y  T)
Thm* T:Type, x,y:T. (x = y 
bandDef pq == if p q else false fi
Thm* p,q:. (pq 
tlambdaDef (x:Tb(x))(x) == b(x)
prop_to_boolDef P == InjCase(lem(P) ; true; false)
Thm* P:Prop. (P 

Syntax:rep_sum has structure: hrep_sum('a'b)

About:
boolbfalsebtrueifthenelseunion
decideapplyuniverseequalmemberprop
all!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

WhoCites Definitions HOLlib Sections NuprlLIB Doc