[STATEMENT]
lemma RS1N_DA[simp]: "removeShadowRules1_alternative (a@[DenyAll]) = [DenyAll]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. removeShadowRules1_alternative (a @ [DenyAll]) = [DenyAll]
[PROOF STEP]
by (simp add: removeShadowRules1_alternative_def)