---

{ [T,A:Type].  x:T. eq:EqDecider(T).  (A  non-void(x : A)) }

{ Proof }

---

Definitions occuring in Statement :  non-void-decl: non-void(d),  fpf-single: x : v,  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  universe: Type,  deq: EqDecider(T)
Definitions :  uall: [x:A]. B[x],  all: x:A. B[x],  implies: P  Q,  non-void-decl: non-void(d),  prop: ,  member: t  T,  so_lambda: x y.t[x; y],  iff: P  Q,  so_apply: x[s1;s2],  and: P  Q,  rev_implies: P  Q
Lemmas :  fpf-all-single-decl,  deq_wf

---

\mforall{}[T,A:Type].    \mforall{}x:T.  \mforall{}eq:EqDecider(T).    (A  {}\mRightarrow{}  non-void(x  :  A))


Date html generated: 2011_08_10-AM-08_09_08
Last ObjectModification: 2011_06_18-AM-08_25_33

Home Index