Nuprl Lemma : ballot-id_wf
ballot-id() 
Type
Proof not projected
Definitions occuring in Statement :
ballot-id: ballot-id(),
member: t T,
universe: Type
Definitions :
universe: Type,
member: t T,
unit: Unit,
equal: s = t,
nat: 
,
product: x:A 
B[x],
union: left + right,
ballot-id: ballot-id()
Lemmas :
nat_wf,
unit_wf
ballot-id() \mmember{} Type
Date html generated:
2011_10_20-PM-04_11_33
Last ObjectModification:
2011_01_29-AM-00_42_29
Home
Index