proposition: Lemma forall_cons {P : T -> Prop} {a s} : {in a::s, forall x, P x} <-> P a /\ {in s, forall x, P x}.
proof: Proof. split=> [A|[A B]]; last by move => x /predU1P [-> //|]; apply: B. by split=> [|b Hb]; apply: A; rewrite !inE ?eqxx ?Hb ?orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)