[STATEMENT]
lemma all_unrest: "x \<sharp> P \<Longrightarrow> (\<forall> x \<bullet> P) = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> P \<Longrightarrow> (\<forall> x \<bullet> P) = P
[PROOF STEP]
by (pred_auto)