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:
match goal with
           | |- ?x = ?y =>
                 let x' := eval hnf in x in
                 let y' := eval hnf in y in
                 change_no_check (x' = y')
           end