proposition: Lemma and6P : reflect [/\ b1, b2, b3, b4, b5 & b6] [&& b1, b2, b3, b4, b5 & b6].
proof: Proof. by case b1; case b2; case b3; case b4; case b5; case b6; constructor; try by case. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun seq) Eqdep ClassicalFacts