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


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::reflexivity@0>