[STATEMENT]
lemma strict_Some [simp]: 
  "(strict f x = OK y) = (\<exists> z. x = OK z \<and> f z = OK y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (strict f x = OK y) = (\<exists>z. x = OK z \<and> f z = OK y)
[PROOF STEP]
by (cases x, auto)