---

{ [T,V:Type]. [A:T  ]. [dcd_A:t:T  Dec(A t)]. [f:{t:T| A t}   V].
  [g:{t:T| (A t)}   V].
    ([A? f : g]  T  V) }

{ Proof }

---

Definitions occuring in Statement :  conditional: [P? f : g],  decidable: Dec(P),  uall: [x:A]. B[x],  prop: ,  not: A,  member: t  T,  set: {x:A| B[x]} ,  apply: f a,  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  prop: ,  member: t  T,  conditional: [P? f : g],  branch: if p:P then A[p] else B fi ,  all: x:A. B[x],  implies: P  Q,  decidable: Dec(P),  or: P  Q
Lemmas :  decidable_wf,  not_wf

---

\mforall{}[T,V:Type].  \mforall{}[A:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[dcd$_{A}$:t:T  {}\mrightarrow{}  Dec(A  t)].  \mforall{}[f:\{t:T|  A  t\}    {}\mrightarrow{}  V].  \mforall{}\000C[g:\{t:T|  \mneg{}(A  t)\}    {}\mrightarrow{}  V].
    ([A?  f  :  g]  \mmember{}  T  {}\mrightarrow{}  V)


Date html generated: 2011_08_16-AM-11_06_02
Last ObjectModification: 2011_06_18-AM-09_38_16

Home Index