Goal:
  
  A : Type
  B : Type
  P : A → B → Prop
  a : A
  l : list A
  f : Forall2 P (a :: l) []
  IHl : ∀ l' : list B, Forall2 P l l' → All2 P l l'
  ============================
   (All2 P (a :: l) [])


DEBUG:Going to execute:
constructor
Level 0: Backtrace:

In environment
A : Type
B : Type
P : A → B → Prop
b : B
l' : list B
f : Forall2 P [] (b :: l')
Unable to unify "All2 ?M2742 (?M2743 :: ?M2745) (?M2744 :: ?M2746)" with
 "All2 P [] (b :: l')".
Level 0: Backtrace:

In environment
A : Type
B : Type
P : A → B → Prop
b : B
l' : list B
f : Forall2 P [] (b :: l')
Unable to unify "All2 ?M2742 (?M2743 :: ?M2745) (?M2744 :: ?M2746)" with
 "All2 P [] (b :: l')".