Goal:
    A : Type  P : list A → list A → A → A → Type  Q : list A → A → Type
  ============================
   (All_fold Q []
    → All_fold Q []
      → All2_fold (λ (Γ Γ' : list A) (x y : A), Q Γ x × Q Γ' y × P Γ Γ' x y)
          [] [])


DEBUG:Going to execute:
constructor