Goal:
    A : Type  B : Type  P : A → B → Type  Q : A → B → Type  l : list A
  ============================
   (∀ l' : list B,
      All2 P l l'
      → (∀ (x : A) (y : B), In x l → In y l' → P x y → Q x y) → All2 Q l l')


DEBUG:Going to execute:
induction l; intros