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