[STATEMENT]
lemma bindET_unitET [simp]:
  "bindET\<cdot>(unitET\<cdot>x)\<cdot>k = k\<cdot>x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bindET\<cdot>(unitET\<cdot>x)\<cdot>k = k\<cdot>x
[PROOF STEP]
by (rule errorT_eqI, simp)