proposition: Theorem eqbPair_prop : forall (A B : Set)(eqda : EqDec A)(eqdb : EqDec B)(p1 p2 : (A * B)), eqbPair _ _ p1 p2 = true -> p1 = p2.
proof: Proof. intuition idtac. unfold eqbPair in *. apply andb_prop in H. intuition idtac. simpl in *. rewrite eqb_leibniz in H0. rewrite eqb_leibniz in H1. subst. destruct p2; trivial. Qed.
imports: Bvector Arith