### Nuprl Lemma : comb_for_lookup_wf

`λa,B,z,k,xs,z1. (xs[k]) ∈ a:PosetSig ⟶ B:Type ⟶ z:B ⟶ k:|a| ⟶ xs:((|a| × B) List) ⟶ (↓True) ⟶ B`

Proof

Definitions occuring in Statement :  lookup: `as[k]` list: `T List` squash: `↓T` true: `True` member: `t ∈ T` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` product: `x:A × B[x]` universe: `Type` set_car: `|p|` poset_sig: `PosetSig`
Definitions unfolded in proof :  member: `t ∈ T` squash: `↓T` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` prop: `ℙ`
Lemmas referenced :  lookup_wf squash_wf true_wf list_wf set_car_wf poset_sig_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaEquality sqequalHypSubstitution imageElimination cut lemma_by_obid dependent_functionElimination thin hypothesisEquality equalityTransitivity hypothesis equalitySymmetry isectElimination productEquality universeEquality

Latex:
\mlambda{}a,B,z,k,xs,z1.  (xs[k])  \mmember{}  a:PosetSig  {}\mrightarrow{}  B:Type  {}\mrightarrow{}  z:B  {}\mrightarrow{}  k:|a|  {}\mrightarrow{}  xs:((|a|  \mtimes{}  B)  List)  {}\mrightarrow{}  (\mdownarrow{}True)  {}\mrightarrow{}  \000CB

Date html generated: 2016_05_16-AM-08_16_39
Last ObjectModification: 2015_12_28-PM-06_27_43

Theory : polynom_2

Home Index