Nuprl Lemma : l_all_append
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀L1,L2:T List. ((∀x∈L1 @ L2.P[x]) ⇐⇒ (∀x∈L1.P[x]) ∧ (∀x∈L2.P[x]))
Proof
Definitions occuring in Statement :
l_all: (∀x∈L.P[x]),
append: as @ bs,
list: T List,
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
member: t ∈ T,
rev_implies: P ⇐ Q,
or: P ∨ Q,
prop: ℙ,
guard: {T},
so_lambda: λ2x.t[x],
so_apply: x[s]
Lemmas referenced :
member_append,
l_member_wf,
all_wf,
append_wf,
l_all_iff,
l_all_wf,
iff_wf,
list_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
cut,
independent_pairFormation,
hypothesis,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
independent_functionElimination,
introduction,
extract_by_obid,
isectElimination,
because_Cache,
productElimination,
inlFormation,
sqequalRule,
inrFormation,
lambdaEquality,
functionEquality,
applyEquality,
unionElimination,
productEquality,
addLevel,
setElimination,
rename,
setEquality,
cumulativity,
universeEquality
Latex:
\mforall{}[T:Type]. \mforall{}[P:T {}\mrightarrow{} \mBbbP{}]. \mforall{}L1,L2:T List. ((\mforall{}x\mmember{}L1 @ L2.P[x]) \mLeftarrow{}{}\mRightarrow{} (\mforall{}x\mmember{}L1.P[x]) \mwedge{} (\mforall{}x\mmember{}L2.P[x]))
Date html generated:
2019_06_20-PM-00_41_36
Last ObjectModification:
2019_01_27-PM-07_11_20
Theory : list_0
Home
Index