Nuprl Lemma : lnk-decl-cap
∀[l:IdLnk]. ∀[dt:tg:Id fp-> Type]. ∀[tg:Id]. ∀[T:Type].  (lnk-decl(l;dt)(rcv(l,tg))?T ~ dt(tg)?T)
Proof
Definitions occuring in Statement : 
lnk-decl: lnk-decl(l;dt)
, 
fpf-cap: f(x)?z
, 
fpf: a:A fp-> B[a]
, 
Kind-deq: KindDeq
, 
rcv: rcv(l,tg)
, 
IdLnk: IdLnk
, 
id-deq: IdDeq
, 
Id: Id
, 
uall: ∀[x:A]. B[x]
, 
universe: Type
, 
sqequal: s ~ t
Lemmas : 
Id_wf, 
fpf_wf, 
IdLnk_wf, 
fpf-dom_wf, 
id-deq_wf, 
subtype-fpf2, 
top_wf, 
subtype_top, 
equal-wf-T-base, 
assert_wf, 
bnot_wf, 
not_wf, 
Knd_wf, 
Kind-deq_wf, 
lnk-decl_wf-hasloc, 
subtype-fpf3, 
hasloc_wf, 
ldst_wf, 
strong-subtype-set2, 
set_wf, 
rcv_wf, 
bool_wf, 
eqtt_to_assert, 
uiff_transitivity, 
eqff_to_assert, 
assert_of_bnot, 
assert-deq-member, 
map_wf, 
member_map, 
subtype_base_sq, 
atom2_subtype_base, 
rcv_one_one, 
l_member_wf
\mforall{}[l:IdLnk].  \mforall{}[dt:tg:Id  fp->  Type].  \mforall{}[tg:Id].  \mforall{}[T:Type].    (lnk-decl(l;dt)(rcv(l,tg))?T  \msim{}  dt(tg)?T)
Date html generated:
2015_07_17-AM-11_15_26
Last ObjectModification:
2015_01_28-AM-07_39_47
Home
Index