ghost-var lib: more lemmas for when you own the two halves

Also, rename ghost_var_op_valid to ghost_var_valid_2, matching own_valid_2. However, there is a possible ambiguity here with using _1/_2 to specifcy left-to-right and right-to-left directions of an equivalence. Also, maybe frac_agree_op_valid should then be renamed as well?