Nuprl Lemma : for_wf
∀[A,B,C:Type]. ∀[f:B ⟶ C ⟶ C]. ∀[k:C]. ∀[as:A List]. ∀[g:A ⟶ B]. (For{A,f,k} x ∈ as. g[x] ∈ C)
Proof
Definitions occuring in Statement :
for: For{T,op,id} x ∈ as. f[x],
list: T List,
uall: ∀[x:A]. B[x],
so_apply: x[s],
member: t ∈ T,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
for: For{T,op,id} x ∈ as. f[x],
tlambda: λx:T. b[x],
so_apply: x[s]
Lemmas referenced :
reduce_wf,
map_wf,
list_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
lambdaEquality,
applyEquality,
hypothesis,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
Error :functionIsType,
Error :universeIsType,
isect_memberEquality,
functionEquality,
because_Cache,
Error :inhabitedIsType,
universeEquality
Latex:
\mforall{}[A,B,C:Type]. \mforall{}[f:B {}\mrightarrow{} C {}\mrightarrow{} C]. \mforall{}[k:C]. \mforall{}[as:A List]. \mforall{}[g:A {}\mrightarrow{} B]. (For\{A,f,k\} x \mmember{} as. g[x] \mmember{} C)
Date html generated:
2019_06_20-PM-00_39_11
Last ObjectModification:
2018_09_26-PM-02_05_45
Theory : list_0
Home
Index