### Nuprl Lemma : A-return'_wf

`∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)].`
`  (A-return'(array-model(AType)) ∈ ⋂T:Type. (T ⟶ (A-map'(array-model(AType)) T)))`

Proof

Definitions occuring in Statement :  A-return': `A-return'(AModel)` A-map': `A-map'(AModel)` array-model: `array-model(AType)` array: `array{i:l}(Val;n)` nat: `ℕ` uall: `∀[x:A]. B[x]` member: `t ∈ T` apply: `f a` isect: `⋂x:A. B[x]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` array-model: `array-model(AType)` A-return': `A-return'(AModel)` A-map': `A-map'(AModel)` pi2: `snd(t)` pi1: `fst(t)` array-monad': `array-monad'(AType)` M-return: `M-return(Mnd)` M-map: `M-map(mnd)` mk_monad: `mk_monad(M;return;bind)`
Lemmas referenced :  array_wf nat_wf Arr_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution hypothesis sqequalRule axiomEquality equalityTransitivity equalitySymmetry lemma_by_obid isectElimination thin hypothesisEquality isect_memberEquality because_Cache universeEquality lambdaEquality

Latex:
\mforall{}[Val:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[AType:array\{i:l\}(Val;n)].
(A-return'(array-model(AType))  \mmember{}  \mcap{}T:Type.  (T  {}\mrightarrow{}  (A-map'(array-model(AType))  T)))

Date html generated: 2016_05_15-PM-02_18_42
Last ObjectModification: 2015_12_27-AM-08_58_42