---

{ [M:Type  Type]
    norm-components  id-fun(component(P.M[P]) List) supposing M[Top] }

{ Proof }

---

Definitions occuring in Statement :  norm-components: norm-components,  component: component(P.M[P]),  uimplies: b supposing a,  uall: [x:A]. B[x],  top: Top,  so_apply: x[s],  member: t  T,  function: x:A  B[x],  list: type List,  universe: Type,  id-fun: id-fun(T)
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  so_apply: x[s],  member: t  T,  norm-components: norm-components,  so_lambda: x.t[x]
Lemmas :  norm-list_wf,  component_wf,  component-has-value,  norm-component_wf,  top_wf

---

\mforall{}[M:Type  {}\mrightarrow{}  Type].  norm-components  \mmember{}  id-fun(component(P.M[P])  List)  supposing  M[Top]


Date html generated: 2011_08_16-PM-06_50_58
Last ObjectModification: 2011_06_18-AM-11_05_30

Home Index