{ 
[T:Type]. [A:EO+(T) 
Type]. [B:Type].
EClass(A[es]) 
r EClass(B) supposing eo:EO+(T). (A[eo] r B) }
{ Proof }
Definitions occuring in Statement :
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
subtype_rel: A r B,
uimplies: b supposing a,
uall: [x:A]. B[x],
so_apply: x[s],
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[s],
eclass: EClass(A[eo; e]),
member: t 
T,
so_lambda: 
x.t[x],
guard: {T}
Lemmas :
subtype_rel_dep_function,
subtype_rel_self,
subtype_rel_function,
top_wf,
subtype_rel_sum,
event-ordering+_wf
\mforall{}[T:Type]. \mforall{}[A:EO+(T) {}\mrightarrow{} Type]. \mforall{}[B:Type].
EClass(A[es]) \msubseteq{}r EClass(B) supposing \mforall{}eo:EO+(T). (A[eo] \msubseteq{}r B)
Date html generated:
2011_08_16-AM-11_28_26
Last ObjectModification:
2011_06_20-AM-00_28_11
Home
Index