### Nuprl Lemma : no_repeats_list-diff

`∀[T:Type]. ∀[L1,L2:T List]. ∀[eq:EqDecider(T)].  no_repeats(T;L1-L2) supposing no_repeats(T;L1)`

Proof

Definitions occuring in Statement :  list-diff: `as-bs` 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 :  list-diff: `as-bs` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` implies: `P `` Q` prop: `ℙ`
Lemmas referenced :  no_repeats_filter bnot_wf deq-member_wf list-diff_wf no_repeats_wf deq_wf list_wf no_repeats_witness
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaEquality hypothesis independent_isectElimination because_Cache universeEquality isect_memberFormation introduction independent_functionElimination sqequalRule isect_memberEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[T:Type].  \mforall{}[L1,L2:T  List].  \mforall{}[eq:EqDecider(T)].    no\_repeats(T;L1-L2)  supposing  no\_repeats(T;L1)

Date html generated: 2016_05_14-PM-03_30_14
Last ObjectModification: 2015_12_26-PM-06_02_44

Theory : decidable!equality

Home Index