Nuprl Lemma : for_hdtl_wf
∀[A,B,C:Type]. ∀[f:B ⟶ C ⟶ C]. ∀[k:C]. ∀[as:A List]. ∀[g:A ⟶ (A List) ⟶ B]. (ForHdTl{A,f,k} h::t ∈ as. g[h;t] ∈ C)
Proof
Definitions occuring in Statement :
for_hdtl: ForHdTl{A,f,k} h::t ∈ as. g[h; t],
list: T List,
uall: ∀[x:A]. B[x],
so_apply: x[s1;s2],
member: t ∈ T,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
for_hdtl: ForHdTl{A,f,k} h::t ∈ as. g[h; t],
so_apply: x[s1;s2]
Lemmas referenced :
reduce_wf,
mapcons_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,
Error :inhabitedIsType,
isect_memberEquality,
functionEquality,
because_Cache,
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{} (A List) {}\mrightarrow{} B].
(ForHdTl\{A,f,k\} h::t \mmember{} as. g[h;t] \mmember{} C)
Date html generated:
2019_06_20-PM-01_19_52
Last ObjectModification:
2018_09_26-PM-05_20_45
Theory : list_1
Home
Index