proposition: Theorem eqbPair_refl : forall (A B : Set)(eqda : EqDec A)(eqdb : EqDec B) (p1 : (A * B)), eqbPair _ _ p1 p1 = true.
proof: Proof. intuition idtac. unfold eqbPair in *. simpl. repeat rewrite eqb_refl. trivial. Qed.
imports: Bvector Arith