Goal:
  
  A : Type
  B : Type
  R : nat → A → B → Type
  n : nat
  x : A
  y : B
  l : list A
  r : list B
  r0 : R n x y
  a : All2i R (S n) l r
  r2 : R n x y
  b : All2i R (S n) l r
  e : apply_noConfusion (x :: l) (x :: l)
        (DepElim.eq_simplification_sigma1 x x l l
           (λ H : x = x,
              DepElim.solution_left x
                (λ (y0 : B) (l0 : list A) (r1 : list B) 
                   (y1 : R n x y0) (a0 : All2i R (S n) l0 r1) 
                   (H0 : l0 = l),
                   DepElim.solution_left l
                     (λ (r2 : list B) (y2 : R n x y0) 
                        (a1 : All2i R (S n) l r2),
                        apply_noConfusion (y0 :: r2) 
                          (y :: r)
                          (DepElim.eq_simplification_sigma1 y0 y r2 r
                             (λ H1 : y0 = y,
                                DepElim.solution_left y
                                  (λ (r3 : list B) 
                                     (y3 : R n x y) 
                                     (a2 : All2i R (S n) l r3) 
                                     (H2 : r3 = r),
                                     DepElim.solution_left r
                                       (λ (y4 : R n x y) 
                                          (a3 : All2i R (S n) l r),
                                          {| pr1 := r0; pr2 := a |} =
                                          {| pr1 := y4; pr2 := a3 |}) r3 H2
                                       y3 a2) y0 H1 r2 y2 a1))) l0 H0 r1 y1
                     a0) x H y l r r2 b)) eq_refl eq_refl
  ============================
   (noConfusionHom_All2i_obligation_2 A B R n (x :: l) 
      (y :: r) (All2i_cons r0 a) (All2i_cons r2 b)
      (noConfusionHom_All2i_obligation_1 A B R n (x :: l) 
         (y :: r) (All2i_cons r0 a) (All2i_cons r2 b) e) = e)


DEBUG:Going to execute:
tac H