Goal:
  
  A : Type
  B : Type
  P : A → B → Prop
  x : A
  y : B
  l : list A
  l' : list B
  H : P x y
  h : Forall2 P l l'
  IHh : Forall2 (λ (x : B) (y : A), P y x) l' l
  ============================
   (Forall2 (λ (x : B) (y : A), P y x) (y :: l') (x :: l))


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

Goals:
  
  A : Type
  B : Type
  P : A → B → Prop
  x : A
  y : B
  l : list A
  l' : list B
  H : P x y
  h : Forall2 P l l'
  IHh : Forall2 (λ (x : B) (y : A), P y x) l' l
  ============================
   (P x y)

  
  A : Type
  B : Type
  P : A → B → Prop
  x : A
  y : B
  l : list A
  l' : list B
  H : P x y
  h : Forall2 P l l'
  IHh : Forall2 (λ (x : B) (y : A), P y x) l' l
  ============================
   (Forall2 (λ (x : B) (y : A), P y x) l' l)


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