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


DEBUG:Going to execute:
induction 1

Goals:
    A : Type  P : list A → A → Type  Q : list A → A → Type
  ============================
   ((∀ (Γ : list A) (x : A), P Γ x → Q Γ x) → All_fold Q [])

  
  A : Type
  P : list A → A → Type
  Q : list A → A → Type
  d : A
  Γ : list A
  X : All_fold P Γ
  p : P Γ d
  IHX : (∀ (Γ : list A) (x : A), P Γ x → Q Γ x) → All_fold Q Γ
  ============================
   ((∀ (Γ : list A) (x : A), P Γ x → Q Γ x) → All_fold Q (d :: Γ))


DEBUG:Going to execute:
simpl

Goals:
    A : Type  P : list A → A → Type  Q : list A → A → Type
  ============================
   ((∀ (Γ : list A) (x : A), P Γ x → Q Γ x) → All_fold Q [])

  
  A : Type
  P : list A → A → Type
  Q : list A → A → Type
  d : A
  Γ : list A
  X : All_fold P Γ
  p : P Γ d
  IHX : (∀ (Γ : list A) (x : A), P Γ x → Q Γ x) → All_fold Q Γ
  ============================
   ((∀ (Γ : list A) (x : A), P Γ x → Q Γ x) → All_fold Q (d :: Γ))


DEBUG:Going to execute:
intros => //