[STATEMENT]
lemma intro_eLet_refine:
  assumes "f x \<le> \<Down>\<^sub>E E R M'"
  shows "Let x f \<le> \<Down>\<^sub>E E R M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Let x f \<le> \<Down>\<^sub>E E R M'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f x \<le> \<Down>\<^sub>E E R M'

goal (1 subgoal):
 1. Let x f \<le> \<Down>\<^sub>E E R M'
[PROOF STEP]
by auto