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


DEBUG:Going to execute:
intros _

Goals:
    A : Type  P : list A → A → Type
  ============================
   (noConfusionHom_All_fold_obligation_1 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) eq_refl) = eq_refl)

  
  A : Type
  P : list A → A → Type
  d : A
  Γ : list A
  a : All_fold P Γ
  p : P Γ d
  ============================
   (noConfusionHom_All_fold_obligation_1 A P (d :: Γ) 
      (All_fold_cons P a p) (All_fold_cons P a p)
      (noConfusionHom_All_fold_obligation_2 A P (d :: Γ)
         (All_fold_cons P a p) (All_fold_cons P a p) eq_refl) = eq_refl)


DEBUG:Going to execute:
CoreTactics.unblock_goal

Goals:
    A : Type  P : list A → A → Type
  ============================
   (noConfusionHom_All_fold_obligation_1 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) eq_refl) = eq_refl)

  
  A : Type
  P : list A → A → Type
  d : A
  Γ : list A
  a : All_fold P Γ
  p : P Γ d
  ============================
   (noConfusionHom_All_fold_obligation_1 A P (d :: Γ) 
      (All_fold_cons P a p) (All_fold_cons P a p)
      (noConfusionHom_All_fold_obligation_2 A P (d :: Γ)
         (All_fold_cons P a p) (All_fold_cons P a p) eq_refl) = eq_refl)


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

Goals:
    A : Type  P : list A → A → Type
  ============================
   (noConfusionHom_All_fold_obligation_1 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) eq_refl) = eq_refl)

  
  A : Type
  P : list A → A → Type
  d : A
  Γ : list A
  a : All_fold P Γ
  p : P Γ d
  ============================
   (noConfusionHom_All_fold_obligation_1 A P (d :: Γ) 
      (All_fold_cons P a p) (All_fold_cons P a p)
      (noConfusionHom_All_fold_obligation_2 A P (d :: Γ)
         (All_fold_cons P a p) (All_fold_cons P a p) eq_refl) = eq_refl)


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

Goals:
    A : Type  P : list A → A → Type
  ============================
   (noConfusionHom_All_fold_obligation_1 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) eq_refl) = eq_refl)

  
  A : Type
  P : list A → A → Type
  d : A
  Γ : list A
  a : All_fold P Γ
  p : P Γ d
  ============================
   (noConfusionHom_All_fold_obligation_1 A P (d :: Γ) 
      (All_fold_cons P a p) (All_fold_cons P a p)
      (noConfusionHom_All_fold_obligation_2 A P (d :: Γ)
         (All_fold_cons P a p) (All_fold_cons P a p) eq_refl) = eq_refl)


DEBUG:Going to execute:
cbv zeta

Goals:
    A : Type  P : list A → A → Type
  ============================
   (noConfusionHom_All_fold_obligation_1 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) eq_refl) = eq_refl)

  
  A : Type
  P : list A → A → Type
  d : A
  Γ : list A
  a : All_fold P Γ
  p : P Γ d
  ============================
   (noConfusionHom_All_fold_obligation_1 A P (d :: Γ) 
      (All_fold_cons P a p) (All_fold_cons P a p)
      (noConfusionHom_All_fold_obligation_2 A P (d :: Γ)
         (All_fold_cons P a p) (All_fold_cons P a p) eq_refl) = eq_refl)


DEBUG:Going to execute:
simpl
Level 2: evaluation returns
idtac of type tacvalue

Level 2: evaluation returns
idtac of type tacvalue


Goals:
    A : Type  P : list A → A → Type
  ============================
   (apply_noConfusion [] []
      (Logic.True_rect_dep
         (λ H : True,
            rew [λ index : list A, All_fold P index]
                match H with
                | I => eq_refl
                end in All_fold_nil P = All_fold_nil P
            → apply_noConfusion [] [] (λ _ : True, True) eq_refl
              → All_fold_nil P = All_fold_nil P)
         (λ H : All_fold_nil P = All_fold_nil P,
            DepElim.solution_left (All_fold_nil P)
              (λ H0 : apply_noConfusion [] [] (λ _ : True, True) eq_refl,
                 match H0 with
                 | I => eq_refl
                 end) (All_fold_nil P) H)) eq_refl eq_refl I = eq_refl)

  
  A : Type
  P : list A → A → Type
  d : A
  Γ : list A
  a : All_fold P Γ
  p : P Γ d
  ============================
   (apply_noConfusion (d :: Γ) (d :: Γ)
      (DepElim.eq_simplification_sigma1_nondep_dep d d Γ Γ
         (λ e' : d = d,
            DepElim.solution_right_dep d
              (λ (Γ0 : list A) (b : All_fold P Γ0) (p0 : P Γ0 d) (e : Γ = Γ0),
                 DepElim.solution_right_dep Γ
                   (λ (b0 : All_fold P Γ) (p1 : P Γ d) 
                      (H : All_fold_cons P a p = All_fold_cons P b0 p1),
                      DepElim.solution_left (All_fold_cons P b0 p1)
                        (λ H0 : apply_noConfusion 
                                  (d :: Γ) (d :: Γ)
                                  (DepElim.eq_simplification_sigma1 d d Γ Γ
                                     (λ H0 : d = d,
                                        DepElim.solution_left d
                                          (λ (Γ1 : list A) 
                                             (a0 : 
                                              All_fold P Γ1) 
                                             (y : P Γ1 d) 
                                             (H1 : Γ1 = Γ),
                                             DepElim.solution_left Γ
                                               (λ (a1 : All_fold P Γ) 
                                                 (y0 : 
                                                 P Γ d),
                                                 {| pr1 := a; pr2 := p |} =
                                                 {| pr1 := a1; pr2 := y0 |})
                                               Γ1 H1 a0 y) d H0 Γ b0 p1))
                                  eq_refl,
                           rew dependent [fun s _ => 
                           All_fold_cons P a p =
                           All_fold_cons P (pr1 s) (pr2 s)] H0 in eq_refl)
                        (All_fold_cons P a p) H) Γ0 e b p0) d e' Γ a p))
      eq_refl eq_refl eq_refl = eq_refl)


DEBUG:Going to execute:
DepElim.simpl_equations

Goals:
    A : Type  P : list A → A → Type
  ============================
   (apply_noConfusion [] []
      (Logic.True_rect_dep
         (λ H : True,
            rew [λ index : list A, All_fold P index]
                match H with
                | I => eq_refl
                end in All_fold_nil P = All_fold_nil P
            → apply_noConfusion [] [] (λ _ : True, True) eq_refl
              → All_fold_nil P = All_fold_nil P)
         (λ H : All_fold_nil P = All_fold_nil P,
            DepElim.solution_left (All_fold_nil P)
              (λ H0 : apply_noConfusion [] [] (λ _ : True, True) eq_refl,
                 match H0 with
                 | I => eq_refl
                 end) (All_fold_nil P) H)) eq_refl eq_refl I = eq_refl)

  
  A : Type
  P : list A → A → Type
  d : A
  Γ : list A
  a : All_fold P Γ
  p : P Γ d
  ============================
   (apply_noConfusion (d :: Γ) (d :: Γ)
      (DepElim.eq_simplification_sigma1_nondep_dep d d Γ Γ
         (λ e' : d = d,
            DepElim.solution_right_dep d
              (λ (Γ0 : list A) (b : All_fold P Γ0) (p0 : P Γ0 d) (e : Γ = Γ0),
                 DepElim.solution_right_dep Γ
                   (λ (b0 : All_fold P Γ) (p1 : P Γ d) 
                      (H : All_fold_cons P a p = All_fold_cons P b0 p1),
                      DepElim.solution_left (All_fold_cons P b0 p1)
                        (λ H0 : apply_noConfusion 
                                  (d :: Γ) (d :: Γ)
                                  (DepElim.eq_simplification_sigma1 d d Γ Γ
                                     (λ H0 : d = d,
                                        DepElim.solution_left d
                                          (λ (Γ1 : list A) 
                                             (a0 : 
                                              All_fold P Γ1) 
                                             (y : P Γ1 d) 
                                             (H1 : Γ1 = Γ),
                                             DepElim.solution_left Γ
                                               (λ (a1 : All_fold P Γ) 
                                                 (y0 : 
                                                 P Γ d),
                                                 {| pr1 := a; pr2 := p |} =
                                                 {| pr1 := a1; pr2 := y0 |})
                                               Γ1 H1 a0 y) d H0 Γ b0 p1))
                                  eq_refl,
                           rew dependent [fun s _ => 
                           All_fold_cons P a p =
                           All_fold_cons P (pr1 s) (pr2 s)] H0 in eq_refl)
                        (All_fold_cons P a p) H) Γ0 e b p0) d e' Γ a p))
      eq_refl eq_refl eq_refl = eq_refl)


DEBUG:Going to execute:
repeat
            (repeat (simpl; DepElim.hnf_eq; DepElim.rewrite_refl_id);
              try progress autounfold with equations)