{ 
Info:Type. n:
. A:n 
Type. Y:i:n EClass(A i). m:. B:m Type.
Z:i:m EClass(B i). T:Type. f:i:n (A i + Top)
i:m (B i + Top)
T + Top
(T + Top).
(f(Y;(Z)';self') 
EClass(T)) }
{ Proof }
Definitions occuring in Statement :
es-rec-combined-interface: f(Y;(Z)';self'),
eclass: EClass(A[eo; e]),
int_seg: {i..j
},
nat: ,
top: Top,
all: x:A. B[x],
member: t T,
apply: f a,
function: x:A B[x],
union: left + right,
natural_number: $n,
universe: Type
Definitions :
equal: s = t,
member: t T,
all: x:A. B[x],
event-ordering+: EO+(Info),
event_ordering: EO,
es-E: E,
universe: Type,
nat: ,
es-rec-combined-interface: f(Y;(Z)';self'),
es-local-pred: last(P),
do-apply: do-apply(f;x),
can-apply: can-apply(f;x),
lambda: 
x.A[x],
eclass-val: X(e),
in-eclass: e 
X,
local-pred-class: local-pred-class(P),
es-prior-interface: prior(X),
es-prior-val: (X)',
eclass: EClass(A[eo; e]),
apply: f a,
union: left + right,
implies: P 
Q,
false: False,
not: 
A,
and: P 
Q,
le: A 
B,
lelt: i j < k,
int: 
,
set: {x:A| B[x]} ,
int_seg: {i..j},
natural_number: $n,
es-causl: (e < e'),
subtype: S 
T,
so_lambda: 
x y.t[x; y],
subtype_rel: A r B,
fpf: a:A fp-> B[a],
strong-subtype: strong-subtype(A;B),
record-select: r.x,
dep-isect: Error :dep-isect,
eq_atom: x =a y,
eq_atom: eq_atom$n(x;y),
record+: record+,
less_than: a < b,
squash: 
T,
real: 
,
grp_car: Error :grp_car,
prop: 
,
true: True,
limited-type: LimitedType,
add: n + m,
void: Void,
subtract: n - m,
minus: -n,
ge: i 
j ,
product: x:A 
B[x],
exists: 
x:A. B[x],
strongwellfounded: SWellFounded(R[x; y]),
isect: 
x:A. B[x],
top: Top,
function: x:A B[x],
isl: isl(x),
assert: 
b,
es-locl: (e <loc e'),
sq_exists: x:A. B[x],
or: P 
Q,
tactic: Error :tactic,
bool: 
,
guard: {T},
infix_ap: x f y,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
ifthenelse: if b then t else f fi ,
pair: <a, b>,
Id: Id,
intensional-universe: IType,
token: "$token",
atom: Atom,
cand: A c B,
es-loc: loc(e),
l_member: (x l),
so_apply: x[s],
Auto: Error :Auto,
CollapseTHEN: Error :CollapseTHEN,
MaAuto: Error :MaAuto,
outl: outl(x),
inl: inl x ,
it: 
,
unit: Unit,
inr: inr x
Lemmas :
it_wf,
unit_wf,
outl_wf,
es-local-pred_wf2,
false_wf,
subtype_rel_self,
intensional-universe_wf,
subtype_rel_wf,
bool_wf,
isl_wf,
assert_wf,
es-locl_wf,
not_wf,
es-causl-swellfnd,
nat_properties,
ge_wf,
es-causl_wf,
le_wf,
nat_wf,
int_seg_wf,
es-prior-val_wf,
eclass_wf,
event-ordering+_inc,
top_wf,
event-ordering+_wf,
member_wf,
es-E_wf
\mforall{}Info:Type. \mforall{}n:\mBbbN{}. \mforall{}A:\mBbbN{}n {}\mrightarrow{} Type. \mforall{}Y:i:\mBbbN{}n {}\mrightarrow{} EClass(A i). \mforall{}m:\mBbbN{}. \mforall{}B:\mBbbN{}m {}\mrightarrow{} Type.
\mforall{}Z:i:\mBbbN{}m {}\mrightarrow{} EClass(B i). \mforall{}T:Type. \mforall{}f:i:\mBbbN{}n {}\mrightarrow{} (A i + Top)
{}\mrightarrow{} i:\mBbbN{}m {}\mrightarrow{} (B i + Top)
{}\mrightarrow{} T + Top
{}\mrightarrow{} (T + Top).
(f(Y;(Z)';self') \mmember{} EClass(T))
Date html generated:
2010_08_27-PM-02_39_45
Last ObjectModification:
2010_03_24-AM-11_44_18
Home
Index