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 : 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:
tac H