---

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

{ Proof }

---

Definitions occuring in Statement :  conditional: [P? f : g],  decidable: Dec(P),  uall: [x:A]. B[x],  prop: ,  apply: f a,  function: x:A  B[x],  universe: Type,  equal: s = t
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,  so_lambda: x.t[x],  decidable: Dec(P),  or: P  Q,  so_apply: x[s]
Lemmas :  decidable_wf,  branch_wf2,  not_wf

---

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


Date html generated: 2011_08_16-AM-11_06_13
Last ObjectModification: 2011_06_18-AM-09_38_28

Home Index