[STATEMENT]
lemma [param]: "(g, id) \<in> rel \<rightarrow> Id_on (Range rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (local.g, id) \<in> local.rel \<rightarrow> Id_on (Range local.rel)
[PROOF STEP]
unfolding rel_inv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (local.g, id) \<in> br local.g (\<lambda>k. k \<in> local.f ` nodes A) \<rightarrow> Id_on (Range (br local.g (\<lambda>k. k \<in> local.f ` nodes A)))
[PROOF STEP]
by (auto simp: in_br_conv)