proposition: Lemma forall_cons (T : eqType) (P : T -> Prop) a s : (forall x, x \in a :: s -> P x) <-> P a /\ (forall x, x \in s -> P x).
proof: Proof. firstorder using mem_head. by apply H; rewrite in_cons H0. rewrite in_cons in H0. case/predU1P : H0 => [->//|]. exact: H1. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)