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: List uall: [x:A]. B[x] prop: so_apply: x[s1;s2] all: x:A. B[x] iff: ⇐⇒ 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: ⇐⇒ Q and: P ∧ Q implies:  Q member: t ∈ T or: P ∨ Q cand: c∧ B prop: guard: {T} so_lambda: λ2x.t[x] so_apply: x[s1;s2] so_apply: x[s] rev_implies:  Q subtype_rel: A ⊆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