[STATEMENT]
lemma graph_map_of_if_distinct_dom: "distinct (map fst al) \<Longrightarrow> graph (map_of al) = set al"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst al) \<Longrightarrow> graph (map_of al) = set al
[PROOF STEP]
unfolding graph_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst al) \<Longrightarrow> {(a, b) |a b. map_of al a = Some b} = set al
[PROOF STEP]
by auto