[STATEMENT]
lemma eprod_rule[refine_vcg]: 
  "\<lbrakk>\<And>a b. p=(a,b) \<Longrightarrow> S a b \<le> ESPEC \<Phi> \<Psi>\<rbrakk> \<Longrightarrow> (case p of (a,b) \<Rightarrow> S a b) \<le> ESPEC \<Phi> \<Psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b. p = (a, b) \<Longrightarrow> S a b \<le> ESPEC \<Phi> \<Psi>) \<Longrightarrow> (case p of (a, b) \<Rightarrow> S a b) \<le> ESPEC \<Phi> \<Psi>
[PROOF STEP]
by (auto split: prod.split)