Nuprl Lemma : es-dt-cap
∀[da:k:Knd fp-> Type]. ∀[l:IdLnk]. ∀[tg:Id]. ∀[T:Top]. (dt(l;da)(tg)?T ~ da(rcv(l,tg))?T)
Proof
Definitions occuring in Statement :
es-dt: dt(l;da),
fpf-cap: f(x)?z,
fpf: a:A fp-> B[a],
Kind-deq: KindDeq,
rcv: rcv(l,tg),
Knd: Knd,
IdLnk: IdLnk,
id-deq: IdDeq,
Id: Id,
uall: ∀[x:A]. B[x],
top: Top,
universe: Type,
sqequal: s ~ t
Lemmas :
subtype_base_sq,
bool_wf,
bool_subtype_base,
iff_imp_equal_bool,
fpf-dom_wf,
Id_wf,
id-deq_wf,
es-dt_wf,
subtype-fpf2,
top_wf,
subtype_top,
Knd_wf,
Kind-deq_wf,
rcv_wf,
es-dt-dom,
assert_wf
\mforall{}[da:k:Knd fp-> Type]. \mforall{}[l:IdLnk]. \mforall{}[tg:Id]. \mforall{}[T:Top]. (dt(l;da)(tg)?T \msim{} da(rcv(l,tg))?T)
Date html generated:
2015_07_17-AM-11_18_04
Last ObjectModification:
2015_01_28-AM-07_37_15
Home
Index