+(* da spostare *)
+
+lemma mem_append : ∀A,x,l1,l2. mem A x (l1@l2) →
+ mem A x l1 ∨ mem A x l2.
+#A #x #l1 elim l1 normalize [/2/]
+#a #tl #Hind #l2 * [#eqxa %1 /2/ |#memx cases (Hind … memx) /3/]
+qed.
+
+let rec split_on A (l:list A) f acc on l ≝
+ match l with
+ [ nil ⇒ 〈acc,nil ?〉
+ | cons a tl ⇒
+ if f a then 〈acc,a::tl〉 else split_on A tl f (a::acc)
+ ].
+
+lemma split_on_spec: ∀A,l,f,acc,res1,res2.
+ split_on A l f acc = 〈res1,res2〉 →
+ (∃l1. res1 = l1@acc ∧
+ reverse ? l1@res2 = l ∧
+ ∀x. mem ? x l1 → f x = false) ∧
+ ∀a,tl. res2 = a::tl → f a = true.
+#A #l #f elim l
+ [#acc #res1 #res2 normalize in ⊢ (%→?); #H destruct %
+ [@(ex_intro … []) % normalize [% % | #x @False_ind]
+ |#a #tl #H destruct
+ ]
+ |#a #tl #Hind #acc #res1 #res2 normalize in ⊢ (%→?);
+ cases (true_or_false (f a)) #Hfa >Hfa normalize in ⊢ (%→?);
+ #H destruct
+ [% [@(ex_intro … []) % normalize [% % | #x @False_ind]
+ |#a1 #tl1 #H destruct (H) //]
+ |cases (Hind (a::acc) res1 res2 H) * #l1 * *
+ #Hres1 #Htl #Hfalse #Htrue % [2:@Htrue] @(ex_intro … (l1@[a])) %
+ [% [>associative_append @Hres1 | >reverse_append <Htl % ]
+ |#x #Hmemx cases (mem_append ???? Hmemx)
+ [@Hfalse | normalize * [#H >H //| @False_ind]
+ ]
+ ]
+ ]
+qed.
+
+axiom mem_reverse: ∀A,l,x. mem A x (reverse ? l) → mem A x l.
+
+lemma split_on_spec_ex: ∀A,l,f.∃l1,l2.
+ l1@l2 = l ∧ (∀x:A. mem ? x l1 → f x = false) ∧
+ ∀a,tl. l2 = a::tl → f a = true.
+#A #l #f @(ex_intro … (reverse … (\fst (split_on A l f []))))
+@(ex_intro … (\snd (split_on A l f [])))
+cases (split_on_spec A l f [ ] ?? (eq_pair_fst_snd …)) * #l1 * *
+>append_nil #Hl1 >Hl1 #Hl #Hfalse #Htrue %
+ [% [@Hl|#x #memx @Hfalse @mem_reverse //] | @Htrue]
+qed.
+