Goal:
  
  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:
let y' := eval hnf in y in
           change_no_check (x' = y')
DEBUG LTAC Evaluated term: (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)
DEBUG LTAC Evaluated term: eq_refl