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; simpl