Nuprl Lemma : lookup-list-map-type-prop
∀[Key,Value:Type].
(valueall-type(lookup-list-map-type(Key;Value))) supposing (valueall-type(Value) and valueall-type(Key))
Proof
Definitions occuring in Statement :
lookup-list-map-type: lookup-list-map-type(Key;Value),
valueall-type: valueall-type(T),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
universe: Type
Lemmas :
list-valueall-type,
product-valueall-type,
equal-wf-base,
lookup-list-map-type_wf,
base_wf,
valueall-type_wf
\mforall{}[Key,Value:Type].
(valueall-type(lookup-list-map-type(Key;Value))) supposing
(valueall-type(Value) and
valueall-type(Key))
Date html generated:
2015_07_17-AM-08_23_43
Last ObjectModification:
2015_04_02-PM-05_44_38
Home
Index