### Nuprl Lemma : newarray_wf

`∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)].  (newarray(AType) ∈ Val ⟶ Arr(AType))`

Proof

Definitions occuring in Statement :  newarray: `newarray(AType)` Arr: `Arr(AType)` array: `array{i:l}(Val;n)` nat: `ℕ` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` array: `array{i:l}(Val;n)` newarray: `newarray(AType)` pi1: `fst(t)` pi2: `snd(t)` Arr: `Arr(AType)`
Lemmas referenced :  array_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin sqequalRule hypothesisEquality hypothesis axiomEquality equalityTransitivity equalitySymmetry lemma_by_obid isectElimination isect_memberEquality because_Cache universeEquality

Latex:
\mforall{}[Val:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[AType:array\{i:l\}(Val;n)].    (newarray(AType)  \mmember{}  Val  {}\mrightarrow{}  Arr(AType))

Date html generated: 2016_05_15-PM-02_17_36
Last ObjectModification: 2015_12_27-AM-08_59_07