[STATEMENT]
lemma oalist_inv_raw_map_val_pair:
  assumes "oalist_inv_raw xs"
  shows "oalist_inv_raw (map_val_pair f xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oalist_inv_raw (map_val_pair f xs)
[PROOF STEP]
by (rule oalist_inv_raw_map_pair, fact assms, auto)