Nuprl Lemma : member-list-to-set

[T:Type]. ∀eq:EqDecider(T). ∀L:T List. ∀a:T.  ((a ∈ list-to-set(eq;L)) ⇐⇒ (a ∈ L))


Proof




Definitions occuring in Statement :  list-to-set: list-to-set(eq;L) l_member: (x ∈ l) list: List deq: EqDecider(T) uall: [x:A]. B[x] all: x:A. B[x] iff: ⇐⇒ Q universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] and: P ∧ Q
Lemmas referenced :  list-to-set-property list_wf deq_wf
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaFormation dependent_functionElimination productElimination universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}L:T  List.  \mforall{}a:T.    ((a  \mmember{}  list-to-set(eq;L))  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  L))



Date html generated: 2016_05_14-PM-03_25_42
Last ObjectModification: 2015_12_26-PM-06_22_36

Theory : decidable!equality


Home Index