### Nuprl Lemma : cons_member

`∀[T:Type]. ∀l:T List. ∀a,x:T.  ((x ∈ [a / l]) `⇐⇒` (x = a ∈ T) ∨ (x ∈ l))`

Proof

Definitions occuring in Statement :  l_member: `(x ∈ l)` cons: `[a / b]` list: `T List` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` or: `P ∨ Q` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  or: `P ∨ Q` rev_implies: `P `` Q` squash: `↓T` sq_stable: `SqStable(P)` uimplies: `b supposing a` prop: `ℙ` nat: `ℕ` cand: `A c∧ B` member: `t ∈ T` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` iff: `P `⇐⇒` Q` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` l_member: `(x ∈ l)` subtract: `n - m` true: `True` less_than': `less_than'(a;b)` top: `Top` subtype_rel: `A ⊆r B` false: `False` not: `¬A` nequal: `a ≠ b ∈ T ` le: `A ≤ B` sq_type: `SQType(T)` guard: `{T}` so_apply: `x[s]` so_lambda: `λ2x.t[x]` uiff: `uiff(P;Q)` decidable: `Dec(P)` cons: `[a / b]` select: `L[n]` less_than: `a < b` nat_plus: `ℕ+`
Rules used in proof :  universeEquality Error :unionIsType,  imageElimination baseClosed imageMemberEquality independent_functionElimination natural_numberEquality independent_isectElimination because_Cache cumulativity Error :inhabitedIsType,  Error :equalityIsType1,  hypothesisEquality rename setElimination thin isectElimination sqequalHypSubstitution hypothesis extract_by_obid introduction cut Error :universeIsType,  Error :productIsType,  independent_pairFormation Error :lambdaFormation_alt,  Error :isect_memberFormation_alt,  computationStep sqequalTransitivity sqequalReflexivity sqequalRule sqequalSubstitution minusEquality Error :isect_memberEquality_alt,  applyEquality addEquality voidElimination Error :dependent_set_memberEquality_alt,  equalitySymmetry equalityTransitivity Error :lambdaEquality_alt,  intEquality instantiate unionElimination dependent_functionElimination productElimination Error :inlFormation_alt,  Error :dependent_pairFormation_alt,  Error :inrFormation_alt

Latex:
\mforall{}[T:Type].  \mforall{}l:T  List.  \mforall{}a,x:T.    ((x  \mmember{}  [a  /  l])  \mLeftarrow{}{}\mRightarrow{}  (x  =  a)  \mvee{}  (x  \mmember{}  l))

Date html generated: 2019_06_20-PM-00_41_03
Last ObjectModification: 2019_02_27-PM-04_21_33

Theory : list_0

Home Index