[STATEMENT]
lemma relabel_agtt_lang [simp]:
  "agtt_lang (relabel_gtt G) = agtt_lang G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. agtt_lang (relabel_gtt G) = agtt_lang G
[PROOF STEP]
by (simp add: agtt_lang_fmap_states_gtt map_fset_to_nat_inj relabel_gtt_def)