Nuprl Lemma : es-dt-dom
∀[l:IdLnk]. ∀[da:k:Knd fp-> Type]. ∀[tg:Id]. uiff(↑tg ∈ dom(dt(l;da));↑rcv(l,tg) ∈ dom(da))
Proof
Definitions occuring in Statement :
es-dt: dt(l;da),
fpf-dom: x ∈ dom(f),
fpf: a:A fp-> B[a],
Kind-deq: KindDeq,
rcv: rcv(l,tg),
Knd: Knd,
IdLnk: IdLnk,
id-deq: IdDeq,
Id: Id,
assert: ↑b,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
universe: Type
Lemmas :
Id_wf,
fpf_wf,
Knd_wf,
IdLnk_wf,
compose-fpf-dom,
isrcv_wf,
bool_wf,
eqtt_to_assert,
eq_lnk_wf,
lnk_wf,
assert-eq-lnk,
tagof_wf,
unit_wf2,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
it_wf,
rcv_wf,
member-fpf-domain,
es-dt_wf,
subtype-fpf2,
top_wf,
subtype_top,
id-deq_wf,
Kind-deq_wf,
assert_wf,
fpf-dom_wf,
iff_wf,
l_member_wf,
fpf-domain_wf,
bool_cases,
assert_of_bnot,
bnot_wf,
not_wf,
squash_wf,
true_wf,
list_wf,
iff_transitivity,
iff_weakening_uiff,
exists_wf,
equal-wf-T-base,
false_wf,
isl_wf,
uiff_transitivity,
and_wf,
btrue_wf,
bfalse_wf,
outl_wf
\mforall{}[l:IdLnk]. \mforall{}[da:k:Knd fp-> Type]. \mforall{}[tg:Id]. uiff(\muparrow{}tg \mmember{} dom(dt(l;da));\muparrow{}rcv(l,tg) \mmember{} dom(da))
Date html generated:
2015_07_17-AM-11_17_56
Last ObjectModification:
2015_01_28-AM-07_37_58
Home
Index