Goal:
  
  A : Type
  P : list A → list A → A → A → Type
  HP : ∀ (Γ Γ' Γ'' : list A) (x y z : A),
         All2_fold P Γ Γ'
         → All2_fold P Γ' Γ''
           → All2_fold P Γ Γ'' → P Γ Γ' x y → P Γ' Γ'' y z → P Γ Γ'' x z
  z : list A
  d : A
  d' : A
  Γ : list A
  Γ' : list A
  H : All2_fold P Γ Γ'
  p : P Γ Γ' d d'
  IHAll2_fold : ∀ z : list A, All2_fold P Γ' z → All2_fold P Γ z
  H'1' : list A
  H'1 : list A
  H' : All2_fold P H'1' H'1
  ============================
   ({| pr1 := d' :: Γ'; pr2 := z |} = {| pr1 := H'1'; pr2 := H'1 |}
    → let H := CoreTactics.block in
      let H0 := CoreTactics.block in All2_fold P (d :: Γ) z)


DEBUG:Going to execute:
destruct p

Goals:
  
  A : Type
  P : list A → list A → A → A → Type
  HP : ∀ (Γ Γ' Γ'' : list A) (x y z : A),
         All2_fold P Γ Γ'
         → All2_fold P Γ' Γ''
           → All2_fold P Γ Γ'' → P Γ Γ' x y → P Γ' Γ'' y z → P Γ Γ'' x z
  z : list A
  d : A
  d' : A
  Γ : list A
  Γ' : list A
  H : All2_fold P Γ Γ'
  p : P Γ Γ' d d'
  IHAll2_fold : ∀ z : list A, All2_fold P Γ' z → All2_fold P Γ z
  ============================
   ({| pr1 := d' :: Γ'; pr2 := z |} = {| pr1 := []; pr2 := [] |}
    → let H := CoreTactics.block in
      let H0 := CoreTactics.block in All2_fold P (d :: Γ) z)

  
  A : Type
  P : list A → list A → A → A → Type
  HP : ∀ (Γ Γ' Γ'' : list A) (x y z : A),
         All2_fold P Γ Γ'
         → All2_fold P Γ' Γ''
           → All2_fold P Γ Γ'' → P Γ Γ' x y → P Γ' Γ'' y z → P Γ Γ'' x z
  z : list A
  d : A
  d' : A
  Γ : list A
  Γ' : list A
  H : All2_fold P Γ Γ'
  p : P Γ Γ' d d'
  IHAll2_fold : ∀ z : list A, All2_fold P Γ' z → All2_fold P Γ z
  d0 : A
  d'0 : A
  Γ0 : list A
  Γ'0 : list A
  H' : All2_fold P Γ0 Γ'0
  p0 : P Γ0 Γ'0 d0 d'0
  ============================
   ({| pr1 := d' :: Γ'; pr2 := z |} =
    {| pr1 := d0 :: Γ0; pr2 := d'0 :: Γ'0 |}
    → let H := CoreTactics.block in
      let H0 := CoreTactics.block in All2_fold P (d :: Γ) z)


DEBUG:Going to execute:
DepElim.simpl_dep_elim

Goals:
  
  A : Type
  P : list A → list A → A → A → Type
  HP : ∀ (Γ Γ' Γ'' : list A) (x y z : A),
         All2_fold P Γ Γ'
         → All2_fold P Γ' Γ''
           → All2_fold P Γ Γ'' → P Γ Γ' x y → P Γ' Γ'' y z → P Γ Γ'' x z
  z : list A
  d : A
  d' : A
  Γ : list A
  Γ' : list A
  H : All2_fold P Γ Γ'
  p : P Γ Γ' d d'
  IHAll2_fold : ∀ z : list A, All2_fold P Γ' z → All2_fold P Γ z
  ============================
   ({| pr1 := d' :: Γ'; pr2 := z |} = {| pr1 := []; pr2 := [] |}
    → let H := CoreTactics.block in
      let H0 := CoreTactics.block in All2_fold P (d :: Γ) z)

  
  A : Type
  P : list A → list A → A → A → Type
  HP : ∀ (Γ Γ' Γ'' : list A) (x y z : A),
         All2_fold P Γ Γ'
         → All2_fold P Γ' Γ''
           → All2_fold P Γ Γ'' → P Γ Γ' x y → P Γ' Γ'' y z → P Γ Γ'' x z
  z : list A
  d : A
  d' : A
  Γ : list A
  Γ' : list A
  H : All2_fold P Γ Γ'
  p : P Γ Γ' d d'
  IHAll2_fold : ∀ z : list A, All2_fold P Γ' z → All2_fold P Γ z
  d0 : A
  d'0 : A
  Γ0 : list A
  Γ'0 : list A
  H' : All2_fold P Γ0 Γ'0
  p0 : P Γ0 Γ'0 d0 d'0
  ============================
   ({| pr1 := d' :: Γ'; pr2 := z |} =
    {| pr1 := d0 :: Γ0; pr2 := d'0 :: Γ'0 |}
    → let H := CoreTactics.block in
      let H0 := CoreTactics.block in All2_fold P (d :: Γ) z)


DEBUG:Going to execute:
DepElim.simplify_dep_elim; DepElim.simplify_IH_hyps;
            DepElim.unblock_dep_elim

Goals:
  
  A : Type
  P : list A → list A → A → A → Type
  HP : ∀ (Γ Γ' Γ'' : list A) (x y z : A),
         All2_fold P Γ Γ'
         → All2_fold P Γ' Γ''
           → All2_fold P Γ Γ'' → P Γ Γ' x y → P Γ' Γ'' y z → P Γ Γ'' x z
  z : list A
  d : A
  d' : A
  Γ : list A
  Γ' : list A
  H : All2_fold P Γ Γ'
  p : P Γ Γ' d d'
  IHAll2_fold : ∀ z : list A, All2_fold P Γ' z → All2_fold P Γ z
  ============================
   ({| pr1 := d' :: Γ'; pr2 := z |} = {| pr1 := []; pr2 := [] |}
    → let H := CoreTactics.block in
      let H0 := CoreTactics.block in All2_fold P (d :: Γ) z)

  
  A : Type
  P : list A → list A → A → A → Type
  HP : ∀ (Γ Γ' Γ'' : list A) (x y z : A),
         All2_fold P Γ Γ'
         → All2_fold P Γ' Γ''
           → All2_fold P Γ Γ'' → P Γ Γ' x y → P Γ' Γ'' y z → P Γ Γ'' x z
  z : list A
  d : A
  d' : A
  Γ : list A
  Γ' : list A
  H : All2_fold P Γ Γ'
  p : P Γ Γ' d d'
  IHAll2_fold : ∀ z : list A, All2_fold P Γ' z → All2_fold P Γ z
  d0 : A
  d'0 : A
  Γ0 : list A
  Γ'0 : list A
  H' : All2_fold P Γ0 Γ'0
  p0 : P Γ0 Γ'0 d0 d'0
  ============================
   ({| pr1 := d' :: Γ'; pr2 := z |} =
    {| pr1 := d0 :: Γ0; pr2 := d'0 :: Γ'0 |}
    → let H := CoreTactics.block in
      let H0 := CoreTactics.block in All2_fold P (d :: Γ) z)


DEBUG:Going to execute:
DepElim.simplify_dep_elim; DepElim.simplify_IH_hyps

Goals:
  
  A : Type
  P : list A → list A → A → A → Type
  HP : ∀ (Γ Γ' Γ'' : list A) (x y z : A),
         All2_fold P Γ Γ'
         → All2_fold P Γ' Γ''
           → All2_fold P Γ Γ'' → P Γ Γ' x y → P Γ' Γ'' y z → P Γ Γ'' x z
  z : list A
  d : A
  d' : A
  Γ : list A
  Γ' : list A
  H : All2_fold P Γ Γ'
  p : P Γ Γ' d d'
  IHAll2_fold : ∀ z : list A, All2_fold P Γ' z → All2_fold P Γ z
  ============================
   ({| pr1 := d' :: Γ'; pr2 := z |} = {| pr1 := []; pr2 := [] |}
    → let H := CoreTactics.block in
      let H0 := CoreTactics.block in All2_fold P (d :: Γ) z)

  
  A : Type
  P : list A → list A → A → A → Type
  HP : ∀ (Γ Γ' Γ'' : list A) (x y z : A),
         All2_fold P Γ Γ'
         → All2_fold P Γ' Γ''
           → All2_fold P Γ Γ'' → P Γ Γ' x y → P Γ' Γ'' y z → P Γ Γ'' x z
  z : list A
  d : A
  d' : A
  Γ : list A
  Γ' : list A
  H : All2_fold P Γ Γ'
  p : P Γ Γ' d d'
  IHAll2_fold : ∀ z : list A, All2_fold P Γ' z → All2_fold P Γ z
  d0 : A
  d'0 : A
  Γ0 : list A
  Γ'0 : list A
  H' : All2_fold P Γ0 Γ'0
  p0 : P Γ0 Γ'0 d0 d'0
  ============================
   ({| pr1 := d' :: Γ'; pr2 := z |} =
    {| pr1 := d0 :: Γ0; pr2 := d'0 :: Γ'0 |}
    → let H := CoreTactics.block in
      let H0 := CoreTactics.block in All2_fold P (d :: Γ) z)


DEBUG:Going to execute:
DepElim.simplify_dep_elim

Goals:
  
  A : Type
  P : list A → list A → A → A → Type
  HP : ∀ (Γ Γ' Γ'' : list A) (x y z : A),
         All2_fold P Γ Γ'
         → All2_fold P Γ' Γ''
           → All2_fold P Γ Γ'' → P Γ Γ' x y → P Γ' Γ'' y z → P Γ Γ'' x z
  z : list A
  d : A
  d' : A
  Γ : list A
  Γ' : list A
  H : All2_fold P Γ Γ'
  p : P Γ Γ' d d'
  IHAll2_fold : ∀ z : list A, All2_fold P Γ' z → All2_fold P Γ z
  ============================
   ({| pr1 := d' :: Γ'; pr2 := z |} = {| pr1 := []; pr2 := [] |}
    → let H := CoreTactics.block in
      let H0 := CoreTactics.block in All2_fold P (d :: Γ) z)

  
  A : Type
  P : list A → list A → A → A → Type
  HP : ∀ (Γ Γ' Γ'' : list A) (x y z : A),
         All2_fold P Γ Γ'
         → All2_fold P Γ' Γ''
           → All2_fold P Γ Γ'' → P Γ Γ' x y → P Γ' Γ'' y z → P Γ Γ'' x z
  z : list A
  d : A
  d' : A
  Γ : list A
  Γ' : list A
  H : All2_fold P Γ Γ'
  p : P Γ Γ' d d'
  IHAll2_fold : ∀ z : list A, All2_fold P Γ' z → All2_fold P Γ z
  d0 : A
  d'0 : A
  Γ0 : list A
  Γ'0 : list A
  H' : All2_fold P Γ0 Γ'0
  p0 : P Γ0 Γ'0 d0 d'0
  ============================
   ({| pr1 := d' :: Γ'; pr2 := z |} =
    {| pr1 := d0 :: Γ0; pr2 := d'0 :: Γ'0 |}
    → let H := CoreTactics.block in
      let H0 := CoreTactics.block in All2_fold P (d :: Γ) z)


DEBUG:Going to execute:
repeat DepElim.simplify_one_dep_elim