[STATEMENT]
lemma not_conflicting_objects_empty_object [elim!]:
  "(sep_heap x) obj_id = None \<Longrightarrow> not_conflicting_objects x y obj_id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sep_heap x obj_id = None \<Longrightarrow> not_conflicting_objects x y obj_id
[PROOF STEP]
by (clarsimp simp: not_conflicting_objects_def)