### Nuprl Lemma : l_all2_cons

`∀[T:Type]. ∀L:T List. ∀[P:T ⟶ T ⟶ ℙ]. ∀u:T. ((∀x<y∈[u / L].P[x;y]) `⇐⇒` (∀y∈L.P[u;y]) ∧ (∀x<y∈L.P[x;y]))`

Proof

Definitions occuring in Statement :  l_all2: `(∀x<y∈L.P[x; y])` l_all: `(∀x∈L.P[x])` cons: `[a / b]` list: `T List` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s1;s2]` 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]` l_all2: `(∀x<y∈L.P[x; y])` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` member: `t ∈ T` or: `P ∨ Q` cand: `A c∧ B` prop: `ℙ` guard: `{T}` so_lambda: `λ2x.t[x]` so_apply: `x[s1;s2]` so_apply: `x[s]` rev_implies: `P `` Q` subtype_rel: `A ⊆r B`
Lemmas referenced :  l_before_wf l_member_wf equal_wf all_wf or_wf cons_before l_all_iff cons_wf l_all_wf iff_wf list_wf and_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut independent_pairFormation hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination inlFormation because_Cache introduction extract_by_obid isectElimination cumulativity sqequalRule inrFormation productEquality lambdaEquality functionEquality applyEquality functionExtensionality productElimination comment addLevel impliesFunctionality allFunctionality setElimination rename setEquality allLevelFunctionality impliesLevelFunctionality andLevelFunctionality universeEquality unionElimination hyp_replacement equalitySymmetry dependent_set_memberEquality applyLambdaEquality

Latex:
\mforall{}[T:Type]
\mforall{}L:T  List.  \mforall{}[P:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}u:T.  ((\mforall{}x<y\mmember{}[u  /  L].P[x;y])  \mLeftarrow{}{}\mRightarrow{}  (\mforall{}y\mmember{}L.P[u;y])  \mwedge{}  (\mforall{}x<y\mmember{}L.P[x;y]))

Date html generated: 2017_10_01-AM-08_34_37
Last ObjectModification: 2017_07_26-PM-04_25_30

Theory : list!

Home Index