[STATEMENT]
lemma scc_root_is_discovered:
    "scc_root s v scc \<Longrightarrow> v \<in> dom (discovered s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. scc_root s v scc \<Longrightarrow> v \<in> dom (discovered s)
[PROOF STEP]
by (simp add: scc_root_def)