{ 
[l:IdLnk]. [dt:tg:Id fp-> Type]. [knd:Knd]. [T:Type].
lnk-decl(l;dt) || knd : T
supposing (
isrcv(knd))
(lnk(knd) = l)
(tag(knd) 
dom(dt))
(T = dt(tag(knd))) }
{ Proof }
Definitions occuring in Statement :
lnk-decl: lnk-decl(l;dt),
fpf-single: x : v,
fpf-compatible: f || g,
fpf-ap: f(x),
fpf-dom: x dom(f),
fpf: a:A fp-> B[a],
Kind-deq: KindDeq,
eq_lnk: a = b,
id-deq: IdDeq,
tagof: tag(k),
lnk: lnk(k),
isrcv: isrcv(k),
Knd: Knd,
IdLnk: IdLnk,
Id: Id,
assert: b,
uimplies: b supposing a,
uall: [x:A]. B[x],
implies: P Q,
universe: Type,
equal: s = t
Definitions :
uall: [x:A]. B[x],
IdLnk: IdLnk,
Id: Id,
Knd: Knd,
uimplies: b supposing a,
implies: P Q,
fpf-ap: f(x),
fpf-compatible: f || g,
fpf-single: x : v,
member: t T,
all: x:A. B[x],
and: P 
Q,
prop: 
,
top: Top,
so_lambda: 
x.t[x],
pi2: snd(t),
lnk-decl: lnk-decl(l;dt),
pi1: fst(t),
rcv: rcv(l,tg),
assert: b,
isrcv: isrcv(k),
isl: isl(x),
btrue: tt,
ifthenelse: if b then t else f fi ,
true: True,
lnk: lnk(k),
outl: outl(x),
fpf-dom: x dom(f),
tagof: tag(k),
iff: P 
Q,
so_apply: x[s],
sq_type: SQType(T),
guard: {T},
fpf: a:A fp-> B[a],
exists: 
x:A. B[x],
rev_implies: P Q
Lemmas :
iff_weakening_uiff,
assert_wf,
fpf-dom_wf,
fpf-single_wf,
fpf-single-dom,
subtype_base_sq,
union_subtype_base,
IdLnk_wf,
product_subtype_base,
atom2_subtype_base,
Kind-deq_wf,
lnk-decl_wf,
fpf-trivial-subtype-top,
Knd_wf,
fpf_wf,
top_wf,
isrcv_wf,
eq_lnk_wf,
lnk_wf,
Id_wf,
id-deq_wf,
tagof_wf,
fpf-ap_wf,
assert-deq-member,
map_wf,
rcv_wf,
member_map,
bool_wf,
bool_subtype_base,
eq_lnk_self
\mforall{}[l:IdLnk]. \mforall{}[dt:tg:Id fp-> Type]. \mforall{}[knd:Knd]. \mforall{}[T:Type].
lnk-decl(l;dt) || knd : T
supposing (\muparrow{}isrcv(knd)) {}\mRightarrow{} (\muparrow{}lnk(knd) = l) {}\mRightarrow{} (\muparrow{}tag(knd) \mmember{} dom(dt)) {}\mRightarrow{} (T = dt(tag(knd)))
Date html generated:
2011_08_10-AM-08_10_58
Last ObjectModification:
2011_06_18-AM-08_26_39
Home
Index