### Nuprl Lemma : remove-repeats-no_repeats-true

`∀T:Type. ∀eq:EqDecider(T). ∀L:T List.  (no_repeats(T;remove-repeats(eq;L)) `⇐⇒` True)`

Proof

Definitions occuring in Statement :  remove-repeats: `remove-repeats(eq;L)` no_repeats: `no_repeats(T;l)` list: `T List` deq: `EqDecider(T)` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` true: `True` universe: `Type`
Definitions unfolded in proof :  all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` and: `P ∧ Q` implies: `P `` Q` true: `True` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` rev_implies: `P `` Q`
Lemmas referenced :  no_repeats_wf remove-repeats_wf remove-repeats-no_repeats true_wf list_wf deq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation natural_numberEquality cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis dependent_functionElimination universeEquality

Latex:
\mforall{}T:Type.  \mforall{}eq:EqDecider(T).  \mforall{}L:T  List.    (no\_repeats(T;remove-repeats(eq;L))  \mLeftarrow{}{}\mRightarrow{}  True)

Date html generated: 2016_05_14-PM-03_26_49
Last ObjectModification: 2015_12_26-PM-06_23_25

Theory : decidable!equality

Home Index