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


DEBUG:Going to execute:
induction 1

Goals:
  
  A : Type
  B : Type
  C : Type
  A' : Type
  B' : Type
  C' : Type
  P : A → B → C → Type
  f : A' → A
  g : B' → B
  h : C' → C
  ============================
   (All3 P (map f []) (map g []) (map h []))

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


DEBUG:Going to execute:
simpl

Goals:
  
  A : Type
  B : Type
  C : Type
  A' : Type
  B' : Type
  C' : Type
  P : A → B → C → Type
  f : A' → A
  g : B' → B
  h : C' → C
  ============================
   (All3 P [] [] [])

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


DEBUG:Going to execute:
constructor

Goals:
  
  A : Type
  B : Type
  C : Type
  A' : Type
  B' : Type
  C' : Type
  P : A → B → C → Type
  f : A' → A
  g : B' → B
  h : C' → C
  ============================
   (All3 P [] [] [])

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


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

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

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


DEBUG:Going to execute:
auto

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

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


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