{ 
[l:IdLnk]. [dt:tg:Id fp-> Type]. [knd:Knd]. [T:Type].
lnk-decl(l;dt) || knd : T
supposing (
isrcv(knd)) 
(lnk(knd) = l) (T = dt(tag(knd))?Void) }
{ Proof }
Definitions occuring in Statement :
lnk-decl: lnk-decl(l;dt),
fpf-single: x : v,
fpf-compatible: f || g,
fpf-cap: f(x)?z,
fpf: a:A fp-> B[a],
Kind-deq: KindDeq,
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,
void: Void,
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-compatible: f || g,
fpf-single: x : v,
member: t 
T,
all: x:A. B[x],
and: P 
Q,
fpf-ap: f(x),
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: a:A fp-> B[a],
subtype: S 
T,
suptype: suptype(S; T),
tagof: tag(k),
fpf-dom: x dom(f),
iff: P 
Q,
so_apply: x[s],
sq_type: SQType(T),
guard: {T},
fpf-cap: f(x)?z,
exists: 
x:A. B[x],
or: P 
Q,
bfalse: ff,
not: 
A,
false: False,
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,
lnk_wf,
fpf-cap_wf,
Id_wf,
id-deq_wf,
tagof_wf,
assert-deq-member,
map_wf,
rcv_wf,
member_map,
bool_wf,
bool_subtype_base,
btrue_wf,
not_wf,
bnot_wf,
bool_cases,
eqtt_to_assert,
uiff_transitivity,
eqff_to_assert,
assert_of_bnot,
l_member_wf
\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{} (lnk(knd) = l) {}\mRightarrow{} (T = dt(tag(knd))?Void)
Date html generated:
2011_08_10-AM-08_11_05
Last ObjectModification:
2011_06_18-AM-08_26_42
Home
Index