Nuprl Lemma : A-bind_wf3
∀[AType:⋃Val:Type.⋃n:ℕ.array{i:l}(Val;n)]
  (A-bind(array-model(AType)) ∈ ⋂T,S:Type.  ((A-map T) ⟶ (T ⟶ (A-map S)) ⟶ (A-map S)))
Proof
Definitions occuring in Statement : 
A-bind: A-bind(AModel)
, 
A-map: A-map
, 
array-model: array-model(AType)
, 
array: array{i:l}(Val;n)
, 
nat: ℕ
, 
tunion: ⋃x:A.B[x]
, 
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
, 
tunion: ⋃x:A.B[x]
, 
pi2: snd(t)
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s]
Lemmas referenced : 
A-bind_wf2, 
tunion_wf, 
nat_wf, 
array_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation, 
cut, 
sqequalHypSubstitution, 
imageElimination, 
productElimination, 
thin, 
sqequalRule, 
lemma_by_obid, 
isectElimination, 
hypothesisEquality, 
hypothesis, 
instantiate, 
universeEquality, 
lambdaEquality, 
cumulativity
Latex:
\mforall{}[AType:\mcup{}Val:Type.\mcup{}n:\mBbbN{}.array\{i:l\}(Val;n)]
    (A-bind(array-model(AType))  \mmember{}  \mcap{}T,S:Type.    ((A-map  T)  {}\mrightarrow{}  (T  {}\mrightarrow{}  (A-map  S))  {}\mrightarrow{}  (A-map  S)))
Date html generated:
2016_05_15-PM-02_18_32
Last ObjectModification:
2015_12_27-AM-08_58_46
Theory : monads
Home
Index