Goal:
  
  A : Type
  P : list A → A → Type
  Q : list A → list A → A → A → Type
  Γ : list A
  ============================
   (All_fold P Γ
    → (∀ (Γ : list A) (d : A),
         All_fold P Γ → All2_fold Q Γ Γ → P Γ d → Q Γ Γ d d)
      → All2_fold Q Γ Γ)


DEBUG:Going to execute:
intros a H; induction a