proposition: Lemma All_cat (s1 s2 : seq T) : All (s1 ++ s2) <-> All s1 /\ All s2.
proof: Proof. split. - by move/AllP=>H; split; apply/AllP=>x Hx; apply/H/Mem_cat; [left|right]. by case=>/AllP H1 /AllP H2; apply/AllP=>x /Mem_cat; case=>Hx; [apply: H1| apply: H2]. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)