Find better name for "emp |- P"

Currently, emp |- P is called bi_valid P and is used as a coercion from PROP to Prop. This turns out to be the right definition for the coercion (i.e., (l |-> v -* l |->{0.5} v * l |->{0.5} v)%I is provable), but the name is dubious: Usually, validity is defined as True |- P. Let's try to find a better name.