Goal:
    A : Type  l : list A  l' : list A
  ============================
   (Forall2 eq l l' → l = l')


DEBUG:Going to execute:
induction 1

Goals:
    A : Type
  ============================
   ([] = [])

  
  A : Type
  x : A
  y : A
  l : list A
  l' : list A
  H : x = y
  H0 : Forall2 eq l l'
  IHForall2 : l = l'
  ============================
   (x :: l = y :: l')


DEBUG:Going to execute:
congruence

Goals:
    A : Type
  ============================
   ([] = [])

  
  A : Type
  x : A
  y : A
  l : list A
  l' : list A
  H : x = y
  H0 : Forall2 eq l l'
  IHForall2 : l = l'
  ============================
   (x :: l = y :: l')


DEBUG:Going to execute:
<coq-core.plugins.cc::cc@0> $1