Goal:
  
  A : Type
  P : list A → list A → A → A → Type
  Q : A → A → Type
  Γ : list A
  Δ : list A
  ============================
   (All2_fold (λ _ _ : list A, Q) Γ Δ <~> All2 Q Γ Δ)


DEBUG:Going to execute:
split; induction 1