Nuprl Lemma : bind-provision_wf
∀[T,S:𝕌']. ∀[x:Provisional(T)]. ∀[f:{t:T| allowed(x) ∧ (t = allow(x) ∈ T)} ⟶ Provisional(S)].
(bind-provision(x;t.f[t]) ∈ Provisional(S))
Proof
Definitions occuring in Statement :
bind-provision: bind-provision(x;t.f[t]),
allow: allow(x),
allowed: allowed(x),
provisional-type: Provisional(T),
uall: ∀[x:A]. B[x],
so_apply: x[s],
and: P ∧ Q,
member: t ∈ T,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
bind-provision: bind-provision(x;t.f[t]),
and: P ∧ Q,
prop: ℙ,
uimplies: b supposing a,
so_apply: x[s],
cand: A c∧ B
Lemmas referenced :
allowed_wf,
allow_wf,
provisional-type_wf,
istype-universe,
provision_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
sqequalHypSubstitution,
hypothesis,
functionIsType,
setIsType,
universeIsType,
hypothesisEquality,
sqequalRule,
productIsType,
introduction,
extract_by_obid,
isectElimination,
thin,
equalityIstype,
because_Cache,
independent_isectElimination,
inhabitedIsType,
instantiate,
universeEquality,
isect_memberEquality_alt,
equalityTransitivity,
equalitySymmetry,
productEquality,
applyEquality,
dependent_set_memberEquality_alt,
independent_pairFormation,
productElimination
Latex:
\mforall{}[T,S:\mBbbU{}']. \mforall{}[x:Provisional(T)]. \mforall{}[f:\{t:T| allowed(x) \mwedge{} (t = allow(x))\} {}\mrightarrow{} Provisional(S)].
(bind-provision(x;t.f[t]) \mmember{} Provisional(S))
Date html generated:
2020_05_20-AM-08_01_07
Last ObjectModification:
2020_05_17-PM-11_55_57
Theory : monads
Home
Index