proposition: Lemma AllP xs : All xs <-> forall x, x \In xs -> P x.
proof: Proof. elim: xs=>[|x xs IH] //=. split; first by case=>H1 /IH H2 z; rewrite InE; case=>[->//|]; apply: H2. move=>H; split; first by apply: H; rewrite InE; left. by apply/IH=>z Z; apply: H; rewrite InE; right. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)