proposition: Lemma forall_consT {T : eqType} {a : T} {s} {P : T -> Type} : (forall b, b \in a :: s -> P b) <-T-> (P a * (forall b, b \in s -> P b)).
proof: Proof. split => [A|[A B] b]. - by split => [|b b_s]; apply: A; rewrite inE ?b_s ?orbT ?eqxx. - rewrite inE. case/orS => [/eqP -> //|]. exact: B. Qed.
imports: mathcomp(all_ssreflect)