### Nuprl Lemma : map-sig-empty_wf

`∀[Key,Value:Type]. ∀[m:map-sig{i:l}(Key;Value)].  (map-sig-empty(m) ∈ map-sig-map(m))`

Proof

Definitions occuring in Statement :  map-sig-empty: `map-sig-empty(m)` map-sig-map: `map-sig-map(m)` map-sig: `map-sig{i:l}(Key;Value)` uall: `∀[x:A]. B[x]` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` map-sig-empty: `map-sig-empty(m)` map-sig-map: `map-sig-map(m)` map-sig: `map-sig{i:l}(Key;Value)` record+: record+ record-select: `r.x` subtype_rel: `A ⊆r B` eq_atom: `x =a y` ifthenelse: `if b then t else f fi ` btrue: `tt` uimplies: `b supposing a` guard: `{T}` so_lambda: `λ2x.t[x]` so_apply: `x[s]` iff: `P `⇐⇒` Q` all: `∀x:A. B[x]` rev_implies: `P `` Q` implies: `P `` 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: `A c∧ B` exposed-bfalse: `exposed-bfalse`

Latex:
\mforall{}[Key,Value:Type].  \mforall{}[m:map-sig\{i:l\}(Key;Value)].    (map-sig-empty(m)  \mmember{}  map-sig-map(m))

Date html generated: 2016_05_17-PM-01_47_25
Last ObjectModification: 2015_12_28-PM-08_51_40

Theory : datatype-signatures

Home Index