Nuprl Lemma : lnk-decl-compatible-single2
∀[l:IdLnk]. ∀[dt:tg:Id fp-> Type]. ∀[knd:Knd]. ∀[T:Type].
lnk-decl(l;dt) || knd : T supposing (↑isrcv(knd)) ⇒ (lnk(knd) = l ∈ IdLnk) ⇒ (T = dt(tag(knd))?Void ∈ Type)
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,
tagof: tag(k),
lnk: lnk(k),
isrcv: isrcv(k),
Knd: Knd,
IdLnk: IdLnk,
id-deq: IdDeq,
Id: Id,
assert: ↑b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
void: Void,
universe: Type,
equal: s = t ∈ T
Lemmas :
fpf-single-dom,
subtype_base_sq,
Knd_wf,
union_subtype_base,
IdLnk_wf,
product_subtype_base,
atom2_subtype_base,
fpf_ap_single_lemma,
assert_wf,
fpf-dom_wf,
Kind-deq_wf,
lnk-decl_wf-hasloc,
subtype-fpf3,
hasloc_wf,
ldst_wf,
top_wf,
strong-subtype-set2,
subtype_top,
set_wf,
fpf-single_wf,
isrcv_wf,
lnk_wf,
fpf-cap_wf,
Id_wf,
id-deq_wf,
tagof_wf,
fpf_wf,
assert-deq-member,
map_wf,
rcv_wf,
member_map,
l_member_wf,
and_wf,
equal_wf,
isrcv_rcv_lemma,
btrue_wf,
bool_wf,
bool_subtype_base,
bool_cases,
eqtt_to_assert,
eqff_to_assert,
assert_of_bnot
\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:
2015_07_17-AM-11_16_08
Last ObjectModification:
2015_01_28-AM-07_38_12
Home
Index