Nuprl Lemma : ballot-none_wf
ballot-none() 
 ballot-id()
Proof not projected
Definitions occuring in Statement : 
ballot-none: ballot-none(), 
ballot-id: ballot-id(), 
member: t 
 T
Definitions : 
int:
, 
member: t 
 T, 
product: x:A 
 B[x], 
equal: s = t, 
it:
, 
inr: inr x , 
ballot-none: ballot-none(), 
ballot-id: ballot-id(), 
Unfold: Error :Unfold, 
CollapseTHEN: Error :CollapseTHEN
Lemmas : 
it_wf
ballot-none()  \mmember{}  ballot-id()
Date html generated:
2011_10_20-PM-04_11_54
Last ObjectModification:
2011_01_26-PM-05_37_32
Home
Index