Goal:
  
  P : E.t -> Prop
  P_Proper : Proper (E.eq ==> impl) P
  s : t
  x : elt
  H : InA E.eq x nil
  H' : P x
  ============================
   (List.Exists P nil)


DEBUG:Going to execute:
inversion H