---

{ [Info,A,B:Type].  (ComponentSpec(A;B)  ') }

{ Proof }

---

Definitions occuring in Statement :  es-component: ComponentSpec(A;B),  uall: [x:A]. B[x],  member: t  T,  universe: Type
Definitions :  uall: [x:A]. B[x],  member: t  T,  es-component: ComponentSpec(A;B),  prop: ,  so_lambda: x y.t[x; y],  so_apply: x[s1;s2],  all: x:A. B[x],  subtype: S  T
Lemmas :  event-ordering+_wf,  eclass_wf,  es-E_wf,  event-ordering+_inc

---

\mforall{}[Info,A,B:Type].    (ComponentSpec(A;B)  \mmember{}  \mBbbU{}')


Date html generated: 2011_08_16-PM-05_56_46
Last ObjectModification: 2011_06_20-AM-01_39_33

Home Index