[STATEMENT]
lemma val_is_vD [elim]:
    fixes ip rt
  assumes "ip\<in>kD(rt)"
      and "the (flag rt ip) = val"
    shows "ip\<in>vD(rt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ip \<in> vD rt
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ip \<in> kD rt
the (flag rt ip) = val

goal (1 subgoal):
 1. ip \<in> vD rt
[PROOF STEP]
unfolding vD_def
[PROOF STATE]
proof (prove)
using this:
ip \<in> kD rt
the (flag rt ip) = val

goal (1 subgoal):
 1. ip \<in> {dip. flag rt dip = Some val}
[PROOF STEP]
by auto