Nuprl Lemma : A-bind'_wf
∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)]. ∀[T,S:Type].
(A-bind'(array-model(AType)) ∈ (A-map'(array-model(AType)) T)
⟶ (T ⟶ (A-map'(array-model(AType)) S))
⟶ (A-map'(array-model(AType)) S))
Proof
Definitions occuring in Statement :
A-bind': A-bind'(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,
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-bind': A-bind'(AModel),
A-map': A-map'(AModel),
pi2: snd(t),
pi1: fst(t),
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
prop: ℙ
Lemmas referenced :
M-bind_wf,
array-monad'_wf,
M-map_wf,
equal_wf,
array_wf,
nat_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
cut,
sqequalRule,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
cumulativity,
hypothesisEquality,
hypothesis,
applyEquality,
lambdaEquality,
equalityTransitivity,
equalitySymmetry,
isectEquality,
universeEquality,
functionEquality,
lambdaFormation,
instantiate,
dependent_functionElimination,
independent_functionElimination,
because_Cache
Latex:
\mforall{}[Val:Type]. \mforall{}[n:\mBbbN{}]. \mforall{}[AType:array\{i:l\}(Val;n)]. \mforall{}[T,S:Type].
(A-bind'(array-model(AType)) \mmember{} (A-map'(array-model(AType)) T)
{}\mrightarrow{} (T {}\mrightarrow{} (A-map'(array-model(AType)) S))
{}\mrightarrow{} (A-map'(array-model(AType)) S))
Date html generated:
2017_10_01-AM-08_44_03
Last ObjectModification:
2017_07_26-PM-04_30_05
Theory : monads
Home
Index