Goal:
  
  A : Type
  P : list A → A → Type
  d : A
  Γ : list A
  a : All_fold P Γ
  p : P Γ d
  b : All_fold P Γ
  p0 : P Γ d
  e : NoConfusionHom_All_fold A P (d :: Γ) (All_fold_cons P a p)
        (All_fold_cons P b p0)
  ============================
   (let H := CoreTactics.block in
    noConfusionHom_All_fold_obligation_2 A P (d :: Γ) 
      (All_fold_cons P a p) (All_fold_cons P b p0)
      (noConfusionHom_All_fold_obligation_1 A P (d :: Γ)
         (All_fold_cons P a p) (All_fold_cons P b p0) e) = e)


DEBUG:Going to execute:
intros _

Goals:
  
  A : Type
  P : list A → A → Type
  e : NoConfusionHom_All_fold A P [] (All_fold_nil P) (All_fold_nil P)
  ============================
   (noConfusionHom_All_fold_obligation_2 A P [] (All_fold_nil P)
      (All_fold_nil P)
      (noConfusionHom_All_fold_obligation_1 A P [] 
         (All_fold_nil P) (All_fold_nil P) e) = e)

  
  A : Type
  P : list A → A → Type
  d : A
  Γ : list A
  a : All_fold P Γ
  p : P Γ d
  b : All_fold P Γ
  p0 : P Γ d
  e : NoConfusionHom_All_fold A P (d :: Γ) (All_fold_cons P a p)
        (All_fold_cons P b p0)
  ============================
   (noConfusionHom_All_fold_obligation_2 A P (d :: Γ) 
      (All_fold_cons P a p) (All_fold_cons P b p0)
      (noConfusionHom_All_fold_obligation_1 A P (d :: Γ)
         (All_fold_cons P a p) (All_fold_cons P b p0) e) = e)


DEBUG:Going to execute:
CoreTactics.unblock_goal

Goals:
  
  A : Type
  P : list A → A → Type
  e : NoConfusionHom_All_fold A P [] (All_fold_nil P) (All_fold_nil P)
  ============================
   (noConfusionHom_All_fold_obligation_2 A P [] (All_fold_nil P)
      (All_fold_nil P)
      (noConfusionHom_All_fold_obligation_1 A P [] 
         (All_fold_nil P) (All_fold_nil P) e) = e)

  
  A : Type
  P : list A → A → Type
  d : A
  Γ : list A
  a : All_fold P Γ
  p : P Γ d
  b : All_fold P Γ
  p0 : P Γ d
  e : NoConfusionHom_All_fold A P (d :: Γ) (All_fold_cons P a p)
        (All_fold_cons P b p0)
  ============================
   (noConfusionHom_All_fold_obligation_2 A P (d :: Γ) 
      (All_fold_cons P a p) (All_fold_cons P b p0)
      (noConfusionHom_All_fold_obligation_1 A P (d :: Γ)
         (All_fold_cons P a p) (All_fold_cons P b p0) e) = e)


DEBUG:Going to execute:
unfold CoreTactics.block in *; cbv zeta

Goals:
  
  A : Type
  P : list A → A → Type
  e : NoConfusionHom_All_fold A P [] (All_fold_nil P) (All_fold_nil P)
  ============================
   (noConfusionHom_All_fold_obligation_2 A P [] (All_fold_nil P)
      (All_fold_nil P)
      (noConfusionHom_All_fold_obligation_1 A P [] 
         (All_fold_nil P) (All_fold_nil P) e) = e)

  
  A : Type
  P : list A → A → Type
  d : A
  Γ : list A
  a : All_fold P Γ
  p : P Γ d
  b : All_fold P Γ
  p0 : P Γ d
  e : NoConfusionHom_All_fold A P (d :: Γ) (All_fold_cons P a p)
        (All_fold_cons P b p0)
  ============================
   (noConfusionHom_All_fold_obligation_2 A P (d :: Γ) 
      (All_fold_cons P a p) (All_fold_cons P b p0)
      (noConfusionHom_All_fold_obligation_1 A P (d :: Γ)
         (All_fold_cons P a p) (All_fold_cons P b p0) e) = e)


DEBUG:Going to execute:
unfold CoreTactics.block in *

Goals:
  
  A : Type
  P : list A → A → Type
  e : NoConfusionHom_All_fold A P [] (All_fold_nil P) (All_fold_nil P)
  ============================
   (noConfusionHom_All_fold_obligation_2 A P [] (All_fold_nil P)
      (All_fold_nil P)
      (noConfusionHom_All_fold_obligation_1 A P [] 
         (All_fold_nil P) (All_fold_nil P) e) = e)

  
  A : Type
  P : list A → A → Type
  d : A
  Γ : list A
  a : All_fold P Γ
  p : P Γ d
  b : All_fold P Γ
  p0 : P Γ d
  e : NoConfusionHom_All_fold A P (d :: Γ) (All_fold_cons P a p)
        (All_fold_cons P b p0)
  ============================
   (noConfusionHom_All_fold_obligation_2 A P (d :: Γ) 
      (All_fold_cons P a p) (All_fold_cons P b p0)
      (noConfusionHom_All_fold_obligation_1 A P (d :: Γ)
         (All_fold_cons P a p) (All_fold_cons P b p0) e) = e)


DEBUG:Going to execute:
cbv zeta

Goals:
  
  A : Type
  P : list A → A → Type
  e : NoConfusionHom_All_fold A P [] (All_fold_nil P) (All_fold_nil P)
  ============================
   (noConfusionHom_All_fold_obligation_2 A P [] (All_fold_nil P)
      (All_fold_nil P)
      (noConfusionHom_All_fold_obligation_1 A P [] 
         (All_fold_nil P) (All_fold_nil P) e) = e)

  
  A : Type
  P : list A → A → Type
  d : A
  Γ : list A
  a : All_fold P Γ
  p : P Γ d
  b : All_fold P Γ
  p0 : P Γ d
  e : NoConfusionHom_All_fold A P (d :: Γ) (All_fold_cons P a p)
        (All_fold_cons P b p0)
  ============================
   (noConfusionHom_All_fold_obligation_2 A P (d :: Γ) 
      (All_fold_cons P a p) (All_fold_cons P b p0)
      (noConfusionHom_All_fold_obligation_1 A P (d :: Γ)
         (All_fold_cons P a p) (All_fold_cons P b p0) e) = e)


DEBUG:Going to execute:
simpl in * |-

Goals:
  
  A : Type
  P : list A → A → Type
  e : apply_noConfusion [] [] (λ _ : True, True) eq_refl
  ============================
   (noConfusionHom_All_fold_obligation_2 A P [] (All_fold_nil P)
      (All_fold_nil P)
      (noConfusionHom_All_fold_obligation_1 A P [] 
         (All_fold_nil P) (All_fold_nil P) e) = e)

  
  A : Type
  P : list A → A → Type
  d : A
  Γ : list A
  a : All_fold P Γ
  p : P Γ d
  b : All_fold P Γ
  p0 : P Γ d
  e : apply_noConfusion (d :: Γ) (d :: Γ)
        (DepElim.eq_simplification_sigma1 d d Γ Γ
           (λ H : d = d,
              DepElim.solution_left d
                (λ (Γ0 : list A) (a0 : All_fold P Γ0) 
                   (y : P Γ0 d) (H0 : Γ0 = Γ),
                   DepElim.solution_left Γ
                     (λ (a1 : All_fold P Γ) (y0 : P Γ d),
                        {| pr1 := a; pr2 := p |} = {| pr1 := a1; pr2 := y0 |})
                     Γ0 H0 a0 y) d H Γ b p0)) eq_refl
  ============================
   (noConfusionHom_All_fold_obligation_2 A P (d :: Γ) 
      (All_fold_cons P a p) (All_fold_cons P b p0)
      (noConfusionHom_All_fold_obligation_1 A P (d :: Γ)
         (All_fold_cons P a p) (All_fold_cons P b p0) e) = e)


DEBUG:Going to execute:
CoreTactics.on_last_hyp
            ltac:(fun id =>
                    hnf in id;
                     CoreTactics.destruct_tele_eq id || DepElim.depelim id)

Goals:
  
  A : Type
  P : list A → A → Type
  e : apply_noConfusion [] [] (λ _ : True, True) eq_refl
  ============================
   (noConfusionHom_All_fold_obligation_2 A P [] (All_fold_nil P)
      (All_fold_nil P)
      (noConfusionHom_All_fold_obligation_1 A P [] 
         (All_fold_nil P) (All_fold_nil P) e) = e)

  
  A : Type
  P : list A → A → Type
  d : A
  Γ : list A
  a : All_fold P Γ
  p : P Γ d
  b : All_fold P Γ
  p0 : P Γ d
  e : apply_noConfusion (d :: Γ) (d :: Γ)
        (DepElim.eq_simplification_sigma1 d d Γ Γ
           (λ H : d = d,
              DepElim.solution_left d
                (λ (Γ0 : list A) (a0 : All_fold P Γ0) 
                   (y : P Γ0 d) (H0 : Γ0 = Γ),
                   DepElim.solution_left Γ
                     (λ (a1 : All_fold P Γ) (y0 : P Γ d),
                        {| pr1 := a; pr2 := p |} = {| pr1 := a1; pr2 := y0 |})
                     Γ0 H0 a0 y) d H Γ b p0)) eq_refl
  ============================
   (noConfusionHom_All_fold_obligation_2 A P (d :: Γ) 
      (All_fold_cons P a p) (All_fold_cons P b p0)
      (noConfusionHom_All_fold_obligation_1 A P (d :: Γ)
         (All_fold_cons P a p) (All_fold_cons P b p0) e) = e)


DEBUG:Going to execute:
fun tac => lazymatch goal with
                      | H:_ |- _ => tac H
                      end

Goals:
  
  A : Type
  P : list A → A → Type
  e : apply_noConfusion [] [] (λ _ : True, True) eq_refl
  ============================
   (noConfusionHom_All_fold_obligation_2 A P [] (All_fold_nil P)
      (All_fold_nil P)
      (noConfusionHom_All_fold_obligation_1 A P [] 
         (All_fold_nil P) (All_fold_nil P) e) = e)

  
  A : Type
  P : list A → A → Type
  d : A
  Γ : list A
  a : All_fold P Γ
  p : P Γ d
  b : All_fold P Γ
  p0 : P Γ d
  e : apply_noConfusion (d :: Γ) (d :: Γ)
        (DepElim.eq_simplification_sigma1 d d Γ Γ
           (λ H : d = d,
              DepElim.solution_left d
                (λ (Γ0 : list A) (a0 : All_fold P Γ0) 
                   (y : P Γ0 d) (H0 : Γ0 = Γ),
                   DepElim.solution_left Γ
                     (λ (a1 : All_fold P Γ) (y0 : P Γ d),
                        {| pr1 := a; pr2 := p |} = {| pr1 := a1; pr2 := y0 |})
                     Γ0 H0 a0 y) d H Γ b p0)) eq_refl
  ============================
   (noConfusionHom_All_fold_obligation_2 A P (d :: Γ) 
      (All_fold_cons P a p) (All_fold_cons P b p0)
      (noConfusionHom_All_fold_obligation_1 A P (d :: Γ)
         (All_fold_cons P a p) (All_fold_cons P b p0) e) = e)


DEBUG:Going to execute:
fun id =>
             hnf in id; CoreTactics.destruct_tele_eq id || DepElim.depelim id

Goals:
  
  A : Type
  P : list A → A → Type
  e : apply_noConfusion [] [] (λ _ : True, True) eq_refl
  ============================
   (noConfusionHom_All_fold_obligation_2 A P [] (All_fold_nil P)
      (All_fold_nil P)
      (noConfusionHom_All_fold_obligation_1 A P [] 
         (All_fold_nil P) (All_fold_nil P) e) = e)

  
  A : Type
  P : list A → A → Type
  d : A
  Γ : list A
  a : All_fold P Γ
  p : P Γ d
  b : All_fold P Γ
  p0 : P Γ d
  e : apply_noConfusion (d :: Γ) (d :: Γ)
        (DepElim.eq_simplification_sigma1 d d Γ Γ
           (λ H : d = d,
              DepElim.solution_left d
                (λ (Γ0 : list A) (a0 : All_fold P Γ0) 
                   (y : P Γ0 d) (H0 : Γ0 = Γ),
                   DepElim.solution_left Γ
                     (λ (a1 : All_fold P Γ) (y0 : P Γ d),
                        {| pr1 := a; pr2 := p |} = {| pr1 := a1; pr2 := y0 |})
                     Γ0 H0 a0 y) d H Γ b p0)) eq_refl
  ============================
   (noConfusionHom_All_fold_obligation_2 A P (d :: Γ) 
      (All_fold_cons P a p) (All_fold_cons P b p0)
      (noConfusionHom_All_fold_obligation_1 A P (d :: Γ)
         (All_fold_cons P a p) (All_fold_cons P b p0) e) = e)


DEBUG:Going to execute:
lazymatch goal with
           | H:_ |- _ => tac H
           end