[STATEMENT]
lemma box_repeated:
  "x >>= (\<Lambda> x'. f >>= (\<Lambda> y'. x >>= body\<cdot>x'\<cdot>y'))
  = x >>= (\<Lambda> x'. f >>= (\<Lambda> y'. body\<cdot>x'\<cdot>y'\<cdot>x'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x >>= (\<Lambda> x'. f >>= (\<Lambda> y'. x >>= body\<cdot>x'\<cdot>y')) = x >>= (\<Lambda> x'. f >>= (\<Lambda> y'. body\<cdot>x'\<cdot>y'\<cdot>x'))
[PROOF STEP]
by (cases x, simp_all)