[STATEMENT]
lemma sup_state_opt_any_Some:
  "P \<turnstile> (Some s) \<le>' X = (\<exists>s'. X = Some s' \<and> P \<turnstile> s \<le>\<^sub>i s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<turnstile> \<lfloor>s\<rfloor> \<le>' X = (\<exists>s'. X = \<lfloor>s'\<rfloor> \<and> P \<turnstile> s \<le>\<^sub>i s')
[PROOF STEP]
by (simp add: sup_state_opt_def Opt.le_def lesub_def)