[STATEMENT]
lemma gmap_gappend[simp]: "gmap f (a @\<^sub>g b) = gmap f a @\<^sub>g gmap f b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gmap f (a @\<^sub>g b) = gmap f a @\<^sub>g gmap f b
[PROOF STEP]
by (unfold gappend_def, induct a, induct b, simp+)