[STATEMENT]
lemma fineD[dest]:
  assumes "d fine s"
  shows "\<And>x k. (x,k) \<in> s \<Longrightarrow> k \<subseteq> d x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x k. (x, k) \<in> s \<Longrightarrow> k \<subseteq> d x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
d fine s

goal (1 subgoal):
 1. \<And>x k. (x, k) \<in> s \<Longrightarrow> k \<subseteq> d x
[PROOF STEP]
unfolding fine_def
[PROOF STATE]
proof (prove)
using this:
\<forall>(x, k)\<in>s. k \<subseteq> d x

goal (1 subgoal):
 1. \<And>x k. (x, k) \<in> s \<Longrightarrow> k \<subseteq> d x
[PROOF STEP]
by auto