fact: Definition eqbOption (A : Set)(dA : EqDec A)(o1 o2 : option A) := match o1 with | None => match o2 with | None => true | Some _ => false end | Some a1 => match o2 with | None => false | Some a2 => (eqb a1 a2) end end.
imports: Bvector Arith