---

{ [Info:Type]. [Z:EClass(Top)]. [X:EClass(E(Z))]. [eo:EO+(Info)]. [e:E].
    X(e)  E(Z) supposing e  X }

{ Proof }

---

Definitions occuring in Statement :  es-E-interface: E(X),  eclass-val: X(e),  in-eclass: e  X,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-E: E,  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  top: Top,  member: t  T,  universe: Type
Definitions :  top: Top,  member: t  T,  all: x:A. B[x],  so_lambda: x y.t[x; y],  uall: [x:A]. B[x],  uimplies: b supposing a,  so_apply: x[s1;s2],  subtype: S  T,  prop:
Lemmas :  es-interface-subtype_rel2,  es-E-interface_wf,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf,  top_wf,  eclass-val_wf,  assert_wf,  in-eclass_wf,  eclass_wf

---

\mforall{}[Info:Type].  \mforall{}[Z:EClass(Top)].  \mforall{}[X:EClass(E(Z))].  \mforall{}[eo:EO+(Info)].  \mforall{}[e:E].
    X(e)  \mmember{}  E(Z)  supposing  \muparrow{}e  \mmember{}\msubb{}  X


Date html generated: 2011_08_16-AM-11_43_46
Last ObjectModification: 2011_06_20-AM-00_34_15

Home Index