Added the definition for setbvd_prop. "set_bvd" and "setbvd_prop" are
both methods for building sets. The former builds set { a(x)  x in s }
from set s where a(x) is a function; the latter builds set
{ x in s  p(x) } from all elements x in s satisfying p(x). Both of
them are very useful. The former is defined by set induction on s; the
latter is defined by member introduction and elimination rules.
