[STATEMENT]
lemma stake_nil[simp]:
  "stake i \<sigma> = [] \<longleftrightarrow> i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (stake i \<sigma> = []) = (i = 0)
[PROOF STEP]
by (cases i; clarsimp)