[STATEMENT]
lemma OK_None_bot [iff]: "OK None \<sqsubseteq>\<^bsub>Err.le (le r)\<^esub> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK None \<sqsubseteq>\<^bsub>Err.le (Opt.le r)\<^esub> x
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OK None \<sqsubseteq>\<^bsub>Err.le (Opt.le r)\<^esub> x
[PROOF STEP]
by (simp add: lesub_def Err.le_def le_def split: option.split err.split)