Goal:
  
  P : E.t -> Prop
  P_Proper : Proper (E.eq ==> impl) P
  s : t
  x : elt
  xs : list elt
  IH : List.Exists P xs <-> (exists x : elt, InA E.eq x xs /\ P x)
  ============================
   (P x \/ List.Exists P xs <->
    (exists x0 : elt, (E.eq x0 x \/ InA E.eq x0 xs) /\ P x0))


DEBUG:Going to execute:
setoid_rewrite IH
DEBUG LTAC Evaluated term: InA_cons
DEBUG LTAC Evaluated term: InA_cons
DEBUG LTAC Evaluated term: InA_cons
DEBUG LTAC Evaluated term: InA_cons
DEBUG LTAC Evaluated term: InA_cons
DEBUG LTAC Evaluated term: InA_cons
DEBUG LTAC Evaluated term: InA_cons
DEBUG LTAC Evaluated term: InA_cons
DEBUG LTAC Evaluated term: InA_cons
DEBUG LTAC Evaluated term: InA_cons
DEBUG LTAC Evaluated term: InA_cons
DEBUG LTAC Evaluated term: InA_cons
DEBUG LTAC Evaluated term: InA_cons
DEBUG LTAC Evaluated term: InA_cons
DEBUG LTAC Evaluated term: InA_cons
DEBUG LTAC Evaluated term: InA_cons
DEBUG LTAC Evaluated term: InA_cons
DEBUG LTAC Evaluated term: InA_cons
DEBUG LTAC Evaluated term: InA_cons
DEBUG LTAC Evaluated term: InA_cons
DEBUG LTAC Evaluated term: InA_cons
DEBUG LTAC Evaluated term: InA_cons