Nuprl Lemma : map-sig-map-vatype

[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)].
  (valueall-type(map-sig-map(m))) supposing (valueall-type(Key) and valueall-type(Value))


Definitions occuring in Statement :  map-sig-map: map-sig-map(m) map-sig: map-sig{i:l}(Key;Value) valueall-type: valueall-type(T) uimplies: supposing a uall: [x:A]. B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a map-sig: map-sig{i:l}(Key;Value) record+: record+ record-select: r.x subtype_rel: A ⊆B eq_atom: =a y ifthenelse: if then else fi  btrue: tt guard: {T} so_lambda: λ2x.t[x] so_apply: x[s] iff: ⇐⇒ Q all: x:A. B[x] rev_implies:  Q implies:  Q and: P ∧ Q prop: deq: EqDecider(T) bool: 𝔹 unit: Unit it: uiff: uiff(P;Q) bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) bnot: ¬bb assert: b false: False band: p ∧b q not: ¬A cand: c∧ B exposed-bfalse: exposed-bfalse map-sig-map: map-sig-map(m) squash: T sq_stable: SqStable(P) valueall-type: valueall-type(T) has-value: (a)↓

\mforall{}[Key,Value:Type].  \mforall{}[m:map-sig\{i:l\}(Key;Value)].
    (valueall-type(map-sig-map(m)))  supposing  (valueall-type(Key)  and  valueall-type(Value))

Date html generated: 2016_05_17-PM-01_46_49
Last ObjectModification: 2016_01_17-AM-11_37_49

Theory : datatype-signatures

Home Index