+
+lemma mem_append: ∀A,a,l1,l2.mem A a (l1@l2) →
+ mem ? a l1 ∨ mem ? a l2.
+#A #a #l1 elim l1
+ [#l2 #mema %2 @mema
+ |#b #tl #Hind #l2 *
+ [#eqab %1 %1 @eqab
+ |#Hmema cases (Hind ? Hmema) -Hmema #Hmema [%1 %2 //|%2 //]
+ ]
+ ]
+qed.
+
+lemma mem_append_l1: ∀A,a,l1,l2.mem A a l1 → mem A a (l1@l2).
+#A #a #l1 #l2 elim l1
+ [whd in ⊢ (%→?); @False_ind
+ |#b #tl #Hind * [#eqab %1 @eqab |#Hmema %2 @Hind //]
+ ]
+qed.
+
+lemma mem_append_l2: ∀A,a,l1,l2.mem A a l2 → mem A a (l1@l2).
+#A #a #l1 #l2 elim l1 [//|#b #tl #Hind #Hmema %2 @Hind //]
+qed.
+
+lemma mem_single: ∀A,a,b. mem A a [b] → a=b.
+#A #a #b * // @False_ind
+qed.
+
+lemma mem_map: ∀A,B.∀f:A→B.∀l,b.
+ mem ? b (map … f l) → ∃a. mem ? a l ∧ f a = b.
+#A #B #f #l elim l
+ [#b normalize @False_ind
+ |#a #tl #Hind #b normalize *
+ [#eqb @(ex_intro … a) /3/
+ |#memb cases (Hind … memb) #a * #mema #eqb
+ @(ex_intro … a) /3/
+ ]
+ ]
+qed.
+
+lemma mem_map_forward: ∀A,B.∀f:A→B.∀a,l.
+ mem A a l → mem B (f a) (map ?? f l).
+ #A #B #f #a #l elim l
+ [normalize @False_ind
+ |#b #tl #Hind *
+ [#eqab <eqab normalize %1 % |#memtl normalize %2 @Hind @memtl]
+ ]
+qed.
+
+(****************************** mem filter ***************************)
+lemma mem_filter: ∀S,f,a,l.
+ mem S a (filter S f l) → mem S a l.
+#S #f #a #l elim l [normalize //]
+#b #tl #Hind normalize (cases (f b)) normalize
+ [* [#eqab %1 @eqab | #H %2 @Hind @H]
+ |#H %2 @Hind @H]
+qed.
+
+lemma mem_filter_true: ∀S,f,a,l.
+ mem S a (filter S f l) → f a = true.
+#S #f #a #l elim l [normalize @False_ind ]
+#b #tl #Hind cases (true_or_false (f b)) #H
+normalize >H normalize [2:@Hind]
+* [#eqab // | @Hind]
+qed.
+
+lemma mem_filter_l: ∀S,f,x,l. (f x = true) → mem S x l →
+mem S x (filter ? f l).
+#S #f #x #l #fx elim l [@False_ind]
+#b #tl #Hind *
+ [#eqxb <eqxb >(filter_true ???? fx) %1 %
+ |#Htl cases (true_or_false (f b)) #fb
+ [>(filter_true ???? fb) %2 @Hind @Htl
+ |>(filter_false ???? fb) @Hind @Htl
+ ]
+ ]
+qed.
+
+lemma filter_case: ∀A,p,l,x. mem ? x l →
+ mem ? x (filter A p l) ∨ mem ? x (filter A (λx.¬ p x) l).
+#A #p #l elim l
+ [#x @False_ind
+ |#a #tl #Hind #x *
+ [#eqxa >eqxa cases (true_or_false (p a)) #Hcase
+ [%1 >(filter_true A tl a p Hcase) %1 %
+ |%2 >(filter_true A tl a ??) [%1 % | >Hcase %]
+ ]
+ |#memx cases (Hind … memx) -memx #memx
+ [%1 cases (true_or_false (p a)) #Hpa
+ [>(filter_true A tl a p Hpa) %2 @memx
+ |>(filter_false A tl a p Hpa) @memx
+ ]
+ |cases (true_or_false (p a)) #Hcase
+ [%2 >(filter_false A tl a) [@memx |>Hcase %]
+ |%2 >(filter_true A tl a) [%2 @memx|>Hcase %]
+ ]
+ ]
+ ]
+ ]
+qed.
+
+lemma filter_length2: ∀A,p,l. |filter A p l|+|filter A (λx.¬ p x) l| = |l|.
+#A #p #l elim l //
+#a #tl #Hind cases (true_or_false (p a)) #Hcase
+ [>(filter_true A tl a p Hcase) >(filter_false A tl a ??)
+ [@(eq_f ?? S) @Hind | >Hcase %]
+ |>(filter_false A tl a p Hcase) >(filter_true A tl a ??)
+ [<plus_n_Sm @(eq_f ?? S) @Hind | >Hcase %]
+ ]
+qed.
+
+(***************************** unique *******************************)
+let rec unique A (l:list A) on l ≝
+ match l with
+ [nil ⇒ True
+ |cons a tl ⇒ ¬ mem A a tl ∧ unique A tl].
+
+lemma unique_filter : ∀S,l,f.
+ unique S l → unique S (filter S f l).
+#S #l #f elim l //
+#a #tl #Hind *
+#memba #uniquetl cases (true_or_false … (f a)) #Hfa
+ [>(filter_true ???? Hfa) %
+ [@(not_to_not … memba) @mem_filter |/2/ ]
+ |>filter_false /2/
+ ]
+qed.
+
+lemma filter_eqb : ∀m,l. unique ? l →
+ (mem ? m l ∧ filter ? (eqb m) l = [m])∨(¬mem ? m l ∧ filter ? (eqb m) l = []).
+#m #l elim l
+ [#_ %2 % [% @False_ind | //]
+ |#a #tl #Hind * #Hmema #Hunique
+ cases (Hind Hunique)
+ [* #Hmemm #Hind %1 % [%2 //]
+ >filter_false // @not_eq_to_eqb_false % #eqma @(absurd ? Hmemm) //
+ |* #Hmemm #Hind cases (decidable_eq_nat m a) #eqma
+ [%1 <eqma % [%1 //] >filter_true [2: @eq_to_eqb_true //] >Hind //
+ |%2 %
+ [@(not_to_not … Hmemm) * // #H @False_ind @(absurd … H) //
+ |>filter_false // @not_eq_to_eqb_false @eqma
+ ]
+ ]
+ ]
+ ]
+qed.
+
+lemma length_filter_eqb: ∀m,l. unique ? l →
+ |filter ? (eqb m) l| ≤ 1.
+#m #l #Huni cases (filter_eqb m l Huni) * #_ #H >H //
+qed.