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


DEBUG:Going to execute:
split
DEBUG LTAC Evaluated term: Hl
DEBUG LTAC Evaluated term: Hl'