### Nuprl Lemma : l_member_wf

`∀[T:Type]. ∀[x:T]. ∀[l:T List].  ((x ∈ l) ∈ ℙ)`

Proof

Definitions occuring in Statement :  l_member: `(x ∈ l)` list: `T List` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` l_member: `(x ∈ l)` so_lambda: `λ2x.t[x]` prop: `ℙ` cand: `A c∧ B` nat: `ℕ` uimplies: `b supposing a` sq_stable: `SqStable(P)` implies: `P `` Q` squash: `↓T` so_apply: `x[s]`
Lemmas referenced :  exists_wf nat_wf less_than_wf length_wf equal_wf select_wf sq_stable__le list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis lambdaEquality productEquality setElimination rename because_Cache cumulativity hypothesisEquality independent_isectElimination natural_numberEquality independent_functionElimination imageMemberEquality baseClosed imageElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[l:T  List].    ((x  \mmember{}  l)  \mmember{}  \mBbbP{})

Date html generated: 2017_04_14-AM-08_36_49
Last ObjectModification: 2017_02_27-PM-03_28_46

Theory : list_0

Home Index