---

{ [T:Type]. (piM(T)  Type) }

{ Proof }

---

Definitions occuring in Statement :  piM: piM(T),  uall: [x:A]. B[x],  member: t  T,  universe: Type
Definitions :  uall: [x:A]. B[x],  member: t  T,  piM: piM(T)
Lemmas :  PiDataVal_wf

---

\mforall{}[T:Type].  (piM(T)  \mmember{}  Type)


Date html generated: 2011_08_17-PM-06_57_29
Last ObjectModification: 2011_06_18-PM-12_35_51

Home Index