{ 
[V:Type]
((v,w:V. Dec(v = w))
(A:Id List. x,y:consensus-rcv(V;A). Dec(x = y))) }
{ Proof }
Definitions occuring in Statement :
consensus-rcv: consensus-rcv(V;A),
Id: Id,
decidable: Dec(P),
uall: [x:A]. B[x],
all: x:A. B[x],
implies: P Q,
list: type List,
universe: Type,
equal: s = t
Definitions :
uall: [x:A]. B[x],
implies: P Q,
all: x:A. B[x],
consensus-rcv: consensus-rcv(V;A),
member: t 
T,
prop: 
,
so_lambda: 
x.t[x],
so_apply: x[s]
Lemmas :
consensus-rcv_wf,
Id_wf,
decidable_wf,
decidable__equal_union,
l_member_wf,
nat_wf,
decidable__equal_product,
decidable__equal_set,
decidable__equal_Id,
decidable__equal_nat
\mforall{}[V:Type]. ((\mforall{}v,w:V. Dec(v = w)) {}\mRightarrow{} (\mforall{}A:Id List. \mforall{}x,y:consensus-rcv(V;A). Dec(x = y)))
Date html generated:
2011_08_16-AM-10_10_33
Last ObjectModification:
2011_06_18-AM-09_03_28
Home
Index