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
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
uimplies: b supposing a
, 
lookup-list-map-type: lookup-list-map-type(Key;Value)
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s]
, 
implies: P 
⇒ Q
, 
all: ∀x:A. B[x]
, 
valueall-type: valueall-type(T)
, 
has-value: (a)↓
, 
prop: ℙ
Latex:
\mforall{}[Key,Value:Type].
    (valueall-type(lookup-list-map-type(Key;Value)))  supposing 
          (valueall-type(Value)  and 
          valueall-type(Key))
Date html generated:
2016_05_17-PM-01_50_38
Last ObjectModification:
2015_12_28-PM-08_50_31
Theory : datatype-signatures
Home
Index