proposition: Theorem eqbPair_symm : forall (A B : Set)(eqda : EqDec A)(eqdb : EqDec B) (p1 p2 : (A * B)), eqbPair _ _ p1 p2 = eqbPair _ _ p2 p1.
proof: Proof. intuition. unfold eqbPair in *. simpl. rewrite eqb_symm. rewrite (eqb_symm b b0). trivial. Qed.
imports: Bvector Arith