{ 
[ra,rt:Id 
Id]. [k:Knd]. (kind-rename(ra;rt;k) 
Knd) }
{ Proof }
Definitions occuring in Statement :
kind-rename: kind-rename(ra;rt;k),
Knd: Knd,
Id: Id,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x]
Definitions :
uall: [x:A]. B[x],
member: t T,
kind-rename: kind-rename(ra;rt;k),
so_lambda: 
x.t[x],
so_lambda: x y.t[x; y],
so_apply: x[s],
so_apply: x[s1;s2]
Lemmas :
kindcase_wf,
Knd_wf,
locl_wf,
Id_wf,
rcv_wf,
IdLnk_wf
\mforall{}[ra,rt:Id {}\mrightarrow{} Id]. \mforall{}[k:Knd]. (kind-rename(ra;rt;k) \mmember{} Knd)
Date html generated:
2011_08_10-AM-07_46_16
Last ObjectModification:
2011_06_18-AM-08_12_07
Home
Index