[STATEMENT]
lemma restrictA_append: "restrictA S (a@b) = restrictA S a @ restrictA S b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrictA S (a @ b) = restrictA S a @ restrictA S b
[PROOF STEP]
unfolding restrict_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filter (\<lambda>(k, v). k \<in> S) (a @ b) = filter (\<lambda>(k, v). k \<in> S) a @ filter (\<lambda>(k, v). k \<in> S) b
[PROOF STEP]
by (rule filter_append)