---

{ [Info,T:Type]. [X:EClass(T)].  (LocBounded(T;X)  ') }

{ Proof }

---

Definitions occuring in Statement :  loc-bounded-class: LocBounded(T;X),  eclass: EClass(A[eo; e]),  uall: [x:A]. B[x],  prop: ,  member: t  T,  universe: Type
Lemmas :  class-loc-bound_wf,  Id_wf,  bag_wf,  event-ordering+_wf,  event-ordering+_inc,  es-E_wf,  eclass_wf

---

\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].    (LocBounded(T;X)  \mmember{}  \mBbbP{}')


Date html generated: 2011_08_16-AM-11_30_02
Last ObjectModification: 2011_06_30-PM-12_20_12

Home Index