### Nuprl Lemma : list-to-set-property

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

Proof

Definitions occuring in Statement :  list-to-set: `list-to-set(eq;L)` no_repeats: `no_repeats(T;l)` l_member: `(x ∈ l)` list: `T List` deq: `EqDecider(T)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` list-to-set: `list-to-set(eq;L)` and: `P ∧ Q` member: `t ∈ T` uimplies: `b supposing a` top: `Top` iff: `P `⇐⇒` Q` implies: `P `` Q` prop: `ℙ` rev_implies: `P `` Q` or: `P ∨ Q` not: `¬A` false: `False` guard: `{T}`
Lemmas referenced :  no_repeats_union nil_wf no_repeats_nil member-union l_member_wf l-union_wf iff_wf or_wf list_wf deq_wf null_nil_lemma btrue_wf member-implies-null-eq-bfalse btrue_neq_bfalse
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation independent_pairFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_isectElimination isect_memberEquality voidElimination voidEquality addLevel productElimination impliesFunctionality because_Cache dependent_functionElimination independent_functionElimination universeEquality unionElimination sqequalRule equalityTransitivity equalitySymmetry inrFormation

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

Date html generated: 2018_05_21-PM-00_51_14
Last ObjectModification: 2018_05_19-AM-06_40_51

Theory : decidable!equality

Home Index