---

{ [Info:Type]. [es:EO+(Info)]. [A:Type]. [X:EClass(A)]. [e:E]. [a:A].
    (X(e)?a  A) }

{ Proof }

---

Definitions occuring in Statement :  es-interface-val?: X(e)?v,  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-E: E,  uall: [x:A]. B[x],  member: t  T,  universe: Type
Definitions :  uall: [x:A]. B[x],  member: t  T,  es-interface-val?: X(e)?v,  ifthenelse: if b then t else f fi ,  all: x:A. B[x],  implies: P  Q,  btrue: tt,  prop: ,  so_lambda: x y.t[x; y],  bfalse: ff,  bool: ,  unit: Unit,  iff: P  Q,  and: P  Q,  so_apply: x[s1;s2],  uimplies: b supposing a,  it: ,  subtype: S  T
Lemmas :  in-eclass_wf,  bool_wf,  iff_weakening_uiff,  assert_wf,  eqtt_to_assert,  eclass-val_wf,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf,  not_wf,  uiff_transitivity,  bnot_wf,  eqff_to_assert,  assert_of_bnot,  eclass_wf

---

\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A:Type].  \mforall{}[X:EClass(A)].  \mforall{}[e:E].  \mforall{}[a:A].    (X(e)?a  \mmember{}  A)


Date html generated: 2011_08_16-PM-04_07_57
Last ObjectModification: 2011_06_20-AM-00_41_34

Home Index