Goal:
    A : Type  P : A → Type  a : A
  ============================
   (P a <~> All P [a])


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

Goals:
    A : Type  P : A → Type  a : A
  ============================
   (P a → All P [a])

    A : Type  P : A → Type  a : A
  ============================
   (All P [a] → P a)


DEBUG:Going to execute:
intros