Goal:
  
  A : Type
  B : Type
  C : Type
  P : A → A → Type
  f : B → C → A
  l : list B
  l' : list C
  l'' : list A
  ============================
   (All3 (λ (x : B) (y : C) (z : A), P (f x y) z) l l' l''
    → All2 P (map2 f l l') l'')


DEBUG:Going to execute:
induction 1

Goals:
    A : Type  B : Type  C : Type  P : A → A → Type  f : B → C → A
  ============================
   (All2 P (map2 f [] []) [])

  
  A : Type
  B : Type
  C : Type
  P : A → A → Type
  f : B → C → A
  x : B
  y : C
  z : A
  l : list B
  l' : list C
  l'' : list A
  r : P (f x y) z
  X : All3 (λ (x : B) (y : C) (z : A), P (f x y) z) l l' l''
  IHX : All2 P (map2 f l l') l''
  ============================
   (All2 P (map2 f (x :: l) (y :: l')) (z :: l''))


DEBUG:Going to execute:
constructor

Goals:
    A : Type  B : Type  C : Type  P : A → A → Type  f : B → C → A
  ============================
   (All2 P (map2 f [] []) [])

  
  A : Type
  B : Type
  C : Type
  P : A → A → Type
  f : B → C → A
  x : B
  y : C
  z : A
  l : list B
  l' : list C
  l'' : list A
  r : P (f x y) z
  X : All3 (λ (x : B) (y : C) (z : A), P (f x y) z) l l' l''
  IHX : All2 P (map2 f l l') l''
  ============================
   (All2 P (map2 f (x :: l) (y :: l')) (z :: l''))


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

Goals:
  
  A : Type
  B : Type
  C : Type
  P : A → A → Type
  f : B → C → A
  x : B
  y : C
  z : A
  l : list B
  l' : list C
  l'' : list A
  r : P (f x y) z
  X : All3 (λ (x : B) (y : C) (z : A), P (f x y) z) l l' l''
  IHX : All2 P (map2 f l l') l''
  ============================
   (P (f x y) z)

  
  A : Type
  B : Type
  C : Type
  P : A → A → Type
  f : B → C → A
  x : B
  y : C
  z : A
  l : list B
  l' : list C
  l'' : list A
  r : P (f x y) z
  X : All3 (λ (x : B) (y : C) (z : A), P (f x y) z) l l' l''
  IHX : All2 P (map2 f l l') l''
  ============================
   (All2 P
      ((fix map2 (l : list B) (l' : list C) {struct l} : list A :=
          match l with
          | [] => []
          | hd :: tl =>
              match l' with
              | [] => []
              | hd' :: tl' => f hd hd' :: map2 tl tl'
              end
          end) l l') l'')


DEBUG:Going to execute:
auto

Goals:
  
  A : Type
  B : Type
  C : Type
  P : A → A → Type
  f : B → C → A
  x : B
  y : C
  z : A
  l : list B
  l' : list C
  l'' : list A
  r : P (f x y) z
  X : All3 (λ (x : B) (y : C) (z : A), P (f x y) z) l l' l''
  IHX : All2 P (map2 f l l') l''
  ============================
   (P (f x y) z)

  
  A : Type
  B : Type
  C : Type
  P : A → A → Type
  f : B → C → A
  x : B
  y : C
  z : A
  l : list B
  l' : list C
  l'' : list A
  r : P (f x y) z
  X : All3 (λ (x : B) (y : C) (z : A), P (f x y) z) l l' l''
  IHX : All2 P (map2 f l l') l''
  ============================
   (All2 P
      ((fix map2 (l : list B) (l' : list C) {struct l} : list A :=
          match l with
          | [] => []
          | hd :: tl =>
              match l' with
              | [] => []
              | hd' :: tl' => f hd hd' :: map2 tl tl'
              end
          end) l l') l'')


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