---

{ [Info:Type]. [A,B:es:EO+(Info)  E  Type].
    EClass(A[es;e]) r EClass(B[es;e]) 
    supposing es:EO+(Info). e:E.  (A[es;e] r B[es;e]) }

{ Proof }

---

Definitions occuring in Statement :  eclass: EClass(A[eo; e]),  event-ordering+: EO+(Info),  es-E: E,  subtype_rel: A r B,  uimplies: b supposing a,  uall: [x:A]. B[x],  so_apply: x[s1;s2],  all: x:A. B[x],  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  all: x:A. B[x],  so_apply: x[s1;s2],  member: t  T,  so_lambda: x y.t[x; y],  subtype: S  T
Lemmas :  dep-eclass_subtype_rel,  es-E_wf,  event-ordering+_inc,  event-ordering+_wf

---

\mforall{}[Info:Type].  \mforall{}[A,B:es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  Type].
    EClass(A[es;e])  \msubseteq{}r  EClass(B[es;e])  supposing  \mforall{}es:EO+(Info).  \mforall{}e:E.    (A[es;e]  \msubseteq{}r  B[es;e])


Date html generated: 2011_08_16-AM-11_39_45
Last ObjectModification: 2011_06_20-AM-00_31_00

Home Index