fact: Definition eqbSum(A B : Set)(dA : EqDec A)(dB : EqDec B)(s1 s2 : (A + B)) := match s1 with | inl a1 => match s2 with | inl a2 => eqb a1 a2 | inr b2 => false end | inr b1 => match s2 with | inl a2 => false | inr b2 => eqb b1 b2 end end.
imports: Bvector Arith