Goal:
    A : Type  l' : list A
  ============================
   (All2 (λ x y : A, x = y) l' l')


DEBUG:Going to execute:
induction l'

Goals:
    A : Type
  ============================
   (All2 (λ x y : A, x = y) [] [])

    A : Type  a : A  l' : list A  IHl' : All2 (λ x y : A, x = y) l' l'
  ============================
   (All2 (λ x y : A, x = y) (a :: l') (a :: l'))


DEBUG:Going to execute:
constructor
DEBUG LTAC Evaluated term: l'

Goals:
    A : Type
  ============================
   (All2 (λ x y : A, x = y) [] [])

    A : Type  a : A  l' : list A  IHl' : All2 (λ x y : A, x = y) l' l'
  ============================
   (All2 (λ x y : A, x = y) (a :: l') (a :: l'))


DEBUG:Going to execute:
<coq-core.plugins.ltac::constructor@0>

Goals:
    A : Type  a : A  l' : list A  IHl' : All2 (λ x y : A, x = y) l' l'
  ============================
   (a = a)

    A : Type  a : A  l' : list A  IHl' : All2 (λ x y : A, x = y) l' l'
  ============================
   (All2 (λ x y : A, x = y) l' l')


DEBUG:Going to execute:
auto

Goals:
    A : Type  a : A  l' : list A  IHl' : All2 (λ x y : A, x = y) l' l'
  ============================
   (a = a)

    A : Type  a : A  l' : list A  IHl' : All2 (λ x y : A, x = y) l' l'
  ============================
   (All2 (λ x y : A, x = y) l' l')


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3