---

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

{ Proof }

---

Definitions occuring in Statement :  decidable: Dec(P),  uall: [x:A]. B[x],  prop: ,  so_apply: x[s],  all: x:A. B[x],  implies: P  Q,  set: {x:A| B[x]} ,  function: x:A  B[x],  list: type List,  universe: Type,  equal: s = t,  l_member: (x  l)
Definitions :  uall: [x:A]. B[x],  implies: P  Q,  all: x:A. B[x],  prop: ,  so_apply: x[s],  member: t  T,  iff: P  Q,  l_all: (xL.P[x]),  and: P  Q,  rev_implies: P  Q,  false: False,  so_lambda: x.t[x],  decidable: Dec(P),  or: P  Q,  not: A,  guard: {T}
Lemmas :  l_member_wf,  decidable_wf,  decidable__l_member,  l_member-set,  decidable_functionality,  l_all_wf2,  list-subtype,  decidable__l_all-better-extract

---

\mforall{}[T:Type]
    ((\mforall{}x,y:T.    Dec(x  =  y))
    {}\mRightarrow{}  (\mforall{}L:T  List
                \mforall{}[P:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}x:\{x:T|  (x  \mmember{}  L)\}  .  Dec(P[x]))  {}\mRightarrow{}  Dec(\mforall{}x:\{x:T|  (x  \mmember{}  L)\}  .  P[x])\000C)))


Date html generated: 2011_08_10-AM-07_48_51
Last ObjectModification: 2011_06_18-AM-08_13_13

Home Index