proposition: Lemma or5P : reflect [\/ b1, b2, b3, b4 | b5] [|| b1, b2, b3, b4 | b5].
proof: Proof. case b1; first by constructor; constructor 1. case b2; first by constructor; constructor 2. case b3; first by constructor; constructor 3. case b4; first by constructor; constructor 4. case b5; first by constructor; constructor 5. by constructor; case. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms) Coq(Classes.Morphisms Program.Basics Program.Tactics) Coq(Relations)