---

{ [A:Type]. [x:A?].  (?[x]  A List) }

{ Proof }

---

Definitions occuring in Statement :  cond-to-list: ?[x],  uall: [x:A]. B[x],  unit: Unit,  member: t  T,  union: left + right,  list: type List,  universe: Type
Definitions :  uall: [x:A]. B[x],  member: t  T,  cond-to-list: ?[x]
Lemmas :  unit_wf

---

\mforall{}[A:Type].  \mforall{}[x:A?].    (?[x]  \mmember{}  A  List)


Date html generated: 2011_08_16-AM-11_01_01
Last ObjectModification: 2011_06_18-AM-09_34_31

Home Index