### Nuprl Lemma : no_repeats-intersection

`∀[A:Type]. ∀eq:EqDecider(A). ∀L1,L2:A List.  (no_repeats(A;L1) `` no_repeats(A;(L1 ⋂ L2)))`

Proof

Definitions occuring in Statement :  l_intersection: `(L1 ⋂ L2)` no_repeats: `no_repeats(T;l)` list: `T List` deq: `EqDecider(T)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` implies: `P `` Q` l_intersection: `(L1 ⋂ L2)` uimplies: `b supposing a` prop: `ℙ`
Lemmas referenced :  no_repeats_filter deq-member_wf no_repeats_wf list_wf deq_wf no_repeats_witness l_intersection_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaEquality cumulativity hypothesis independent_isectElimination sqequalRule dependent_functionElimination independent_functionElimination because_Cache universeEquality

Latex:
\mforall{}[A:Type].  \mforall{}eq:EqDecider(A).  \mforall{}L1,L2:A  List.    (no\_repeats(A;L1)  {}\mRightarrow{}  no\_repeats(A;(L1  \mcap{}  L2)))

Date html generated: 2018_05_21-PM-00_51_31
Last ObjectModification: 2017_10_11-PM-02_12_24

Theory : decidable!equality

Home Index