2 focused subgoals (unfocused: 0-0-1)
, subgoal 1 (ID 921)

  A : Type
  B : Type
  f : A -> B
  x' : A
  l' : list A
  y : B
  IHl' : In y (map f l') -> exists x : A, f x = y /\ In x l'
  H2 : exists x : A, f x = y /\ In x l'
  ============================
   f x' = y

subgoal 2 (ID 919) is:
 In x' (x' :: l')