---

{ [T:Type]. ((x,y:T.  Dec(x = y))  (L:T List. finite-type({x:T| (x  L)} ))\000C) }

{ Proof }

---

Definitions occuring in Statement :  decidable: Dec(P),  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  set: {x:A| B[x]} ,  list: type List,  universe: Type,  equal: s = t,  l_member: (x  l),  finite-type: finite-type(T)
Definitions :  uall: [x:A]. B[x],  implies: P  Q,  all: x:A. B[x],  member: t  T,  prop: ,  top: Top,  subtype: S  T
Lemmas :  cardinality-le-finite,  l_member_wf,  length_wf_nat,  top_wf,  decidable_wf,  cardinality-le-list-set

---

\mforall{}[T:Type].  ((\mforall{}x,y:T.    Dec(x  =  y))  {}\mRightarrow{}  (\mforall{}L:T  List.  finite-type(\{x:T|  (x  \mmember{}  L)\}  )))


Date html generated: 2011_08_10-AM-07_48_48
Last ObjectModification: 2011_06_18-AM-08_13_11

Home Index