{ 
[ra,rt:Id 
Id].
(Inj(Knd;Knd;
k.kind-rename(ra;rt;k))) supposing
(Inj(Id;Id;ra) and
Inj(Id;Id;rt)) }
{ Proof }
Definitions occuring in Statement :
kind-rename: kind-rename(ra;rt;k),
Knd: Knd,
Id: Id,
inject: Inj(A;B;f),
uimplies: b supposing a,
uall: [x:A]. B[x],
lambda: x.A[x],
function: x:A B[x]
Definitions :
uall: [x:A]. B[x],
uimplies: b supposing a,
inject: Inj(A;B;f),
kind-rename: kind-rename(ra;rt;k),
all: x:A. B[x],
implies: P 
Q,
locl: locl(a),
rcv: rcv(l,tg),
member: t 
T,
squash: 
T,
true: True,
prop: 
,
so_lambda: 
x.t[x],
so_lambda: x y.t[x; y],
Knd: Knd,
kindcase: kindcase(k;a.f[a];l,t.g[l; t]),
ifthenelse: if b then t else f fi ,
islocal: islocal(k),
actof: act(k),
lnk: lnk(k),
tagof: tag(k),
bnot: 
b,
isl: isl(x),
outr: outr(x),
pi1: fst(t),
outl: outl(x),
pi2: snd(t),
btrue: tt,
bfalse: ff,
guard: {T},
and: P 
Q,
false: False,
so_apply: x[s],
so_apply: x[s1;s2]
Lemmas :
rcv_one_one,
rcv_wf,
squash_wf,
true_wf,
Id_wf,
IdLnk_wf,
not_locl_rcv,
not_rcv_locl,
locl_one_one,
locl_wf,
Knd_wf,
kindcase_wf
\mforall{}[ra,rt:Id {}\mrightarrow{} Id].
(Inj(Knd;Knd;\mlambda{}k.kind-rename(ra;rt;k))) supposing (Inj(Id;Id;ra) and Inj(Id;Id;rt))
Date html generated:
2011_08_10-AM-07_46_24
Last ObjectModification:
2011_06_18-AM-08_12_09
Home
Index