[STATEMENT]
lemma OK_le_err_OK:
  "(OK x <=_(le r) OK y) = (x <=_r y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (OK x \<sqsubseteq>\<^bsub>le r\<^esub> OK y) = (x \<sqsubseteq>\<^bsub>r\<^esub> y)
[PROOF STEP]
by (simp add: unfold_lesub_err le_def)