Goal:
    P : elt -> Prop  s : t
  ============================
   (For_all P s <-> (forall v : elt, In v s -> P v))


DEBUG:Going to execute:
reflexivity