### Nuprl Lemma : no_repeats-insert

`∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[a:T]. ∀[L:T List].  no_repeats(T;insert(a;L)) supposing no_repeats(T;L)`

Proof

Definitions occuring in Statement :  insert: `insert(a;L)` no_repeats: `no_repeats(T;l)` list: `T List` deq: `EqDecider(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` and: `P ∧ Q` uimplies: `b supposing a` implies: `P `` Q` prop: `ℙ`
Lemmas referenced :  insert_property no_repeats_witness insert_wf no_repeats_wf list_wf
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality introduction dependent_functionElimination productElimination sqequalRule isect_memberEquality independent_functionElimination equalityTransitivity equalitySymmetry because_Cache universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[a:T].  \mforall{}[L:T  List].
no\_repeats(T;insert(a;L))  supposing  no\_repeats(T;L)

Date html generated: 2016_05_14-AM-06_54_09
Last ObjectModification: 2015_12_26-PM-00_19_50

Theory : list_0

Home Index