[STATEMENT]
lemma in_targetsI [intro, simp]:
    assumes "ide b" and "trg t \<frown> b"
    shows "b \<in> targets t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<in> targets t
[PROOF STEP]
using assms targets_def resid_arr_self
[PROOF STATE]
proof (prove)
using this:
ide b
trg t \<frown> b
targets ?t = {b. ide b \<and> trg ?t \<frown> b}
?t \ ?t = trg ?t

goal (1 subgoal):
 1. b \<in> targets t
[PROOF STEP]
by simp