Nuprl Lemma : ma-valtype-subtype
∀[k:Knd]. ∀[da,da':a:Knd fp-> Type]. Valtype(da';k) ⊆r Valtype(da;k) supposing da ⊆ da'
Proof
Definitions occuring in Statement :
ma-valtype: Valtype(da;k),
fpf-sub: f ⊆ g,
fpf: a:A fp-> B[a],
Kind-deq: KindDeq,
Knd: Knd,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
universe: Type
Lemmas :
subtype-fpf-cap-top,
top_wf,
fpf-sub_wf,
Knd_wf,
Kind-deq_wf,
fpf_wf
\mforall{}[k:Knd]. \mforall{}[da,da':a:Knd fp-> Type]. Valtype(da';k) \msubseteq{}r Valtype(da;k) supposing da \msubseteq{} da'
Date html generated:
2015_07_17-AM-11_17_27
Last ObjectModification:
2015_01_28-AM-07_37_25
Home
Index