proposition: Lemma or3P : reflect [\/ b1, b2 | b3] [|| b1, b2 | b3].
proof: Proof. case b1; first by constructor; constructor 1. case b2; first by constructor; constructor 2. case b3; first by constructor; constructor 3. by constructor; case. Qed.
imports: ssreflect ssrfun