Goal:
    A : Type  x : A  l : list A
  ============================
   ((∃ y : A, x = y ∧ In y l) ↔ In x l)


DEBUG:Going to execute:
<coq-core.plugins.firstorder::firstorder@0> $1 $2
DEBUG LTAC Evaluated term: InA_alt

Debug:
  
  A : Type
  x : A
  l : list A
  ============================
  (∃ y : A, x = y ∧ In y l) ↔ In x l
Debug:
  
  A : Type
  x : A
  l : list A
  ============================
  (∃ y : A, x = y ∧ In y l) → In x l
Debug:
  
  A : Type
  x : A
  l : list A
  H : ∃ y : A, x = y ∧ In y l
  ============================
  In x l
Debug:
  
  A : Type
  x : A
  l : list A
  x0 : A
  H : x = x0 ∧ In x0 l
  ============================
  In x l
Debug:
  
  A : Type
  x : A
  l : list A
  x0 : A
  H : x = x0
  H0 : In x0 l
  ============================
  In x l
Debug:
  
  A : Type
  x : A
  l : list A
  ============================
  In x l → ∃ y : A, x = y ∧ In y l
Debug:
  
  A : Type
  x : A
  l : list A
  H : In x l
  ============================
  ∃ y : A, x = y ∧ In y l
Debug:
  
  A : Type
  x : A
  l : list A
  H : In x l
  ============================
  x = x ∧ In x l
Debug:   
         A : Type
         x : A
         l : list A
         H : In x l
         ============================
         x = x
Debug:   
         A : Type
         x : A
         l : list A
         H : In x l
         ============================
         In x l