proposition: Lemma all_merge (T : Type) (P : {pred T}) (leT : rel T) s1 s2 : all P (merge leT s1 s2) = all P s1 && all P s2.
proof: Proof. elim: s1 s2 => //= x s1 IHs1; elim=> [|y s2 IHs2]; rewrite ?andbT //=. by case: ifP => _; rewrite /= ?IHs1 ?IHs2 //=; bool_congr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)