### Nuprl Lemma : set-sig-set-vatype

`∀[Item:Type]. ∀[s:set-sig{i:l}(Item)].  valueall-type(set-sig-set(s)) supposing valueall-type(Item)`

Proof

Definitions occuring in Statement :  set-sig-set: `set-sig-set(s)` set-sig: `set-sig{i:l}(Item)` 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` set-sig: `set-sig{i:l}(Item)` 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` implies: `P `` Q` guard: `{T}` so_lambda: `λ2x.t[x]` so_apply: `x[s]` all: `∀x:A. B[x]` prop: `ℙ` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` and: `P ∧ Q` or: `P ∨ Q` set-sig-set: `set-sig-set(s)` squash: `↓T` sq_stable: `SqStable(P)` valueall-type: `valueall-type(T)` has-value: `(a)↓`

Latex:
\mforall{}[Item:Type].  \mforall{}[s:set-sig\{i:l\}(Item)].    valueall-type(set-sig-set(s))  supposing  valueall-type(Item)

Date html generated: 2016_05_17-PM-01_44_12
Last ObjectModification: 2016_01_17-AM-11_37_48

Theory : datatype-signatures

Home Index