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
  ============================
   (apply_noConfusion (x :: l) (x :: l)
      (DepElim.eq_simplification_sigma1_nondep_dep x x l l
         (λ e' : x = x,
            DepElim.solution_right_dep x
              (λ (y0 : B) (l0 : list A) (r1 : list B) 
                 (r2 : R n x y0) (b : All2i R (S n) l0 r1) 
                 (e : l = l0),
                 DepElim.solution_right_dep l
                   (λ (r3 : list B) (r4 : R n x y0) (b0 : All2i R (S n) l r3),
                      apply_noConfusion (y :: r) (y0 :: r3)
                        (DepElim.eq_simplification_sigma1_nondep_dep y y0 r
                           r3
                           (λ e'0 : y = y0,
                              DepElim.solution_right_dep y
                                (λ (r5 : list B) (r6 : R n x y) 
                                   (b1 : All2i R (S n) l r5) 
                                   (e0 : r = r5),
                                   DepElim.solution_right_dep r
                                     (λ (r7 : R n x y) 
                                        (b2 : All2i R (S n) l r) 
                                        (H : All2i_cons r0 a =
                                             All2i_cons r7 b2),
                                        DepElim.solution_left
                                          (All2i_cons r7 b2)
                                          (λ H0 : 
                                              apply_noConfusion 
                                                (x :: l) 
                                                (x :: l)
                                                (DepElim.eq_simplification_sigma1
                                                 x x l l
                                                 (λ H0 : x = x,
                                                 DepElim.solution_left x
                                                 (λ (y1 : B) 
                                                 (l1 : list A) 
                                                 (r8 : list B) 
                                                 (y2 : 
                                                 R n x y1) 
                                                 (a0 : 
                                                 All2i R (S n) l1 r8) 
                                                 (H1 : 
                                                 l1 = l),
                                                 DepElim.solution_left l
                                                 (λ (r9 : list B) 
                                                 (y3 : 
                                                 R n x y1) 
                                                 (a1 : 
                                                 All2i R (S n) l r9),
                                                 apply_noConfusion 
                                                 (y1 :: r9) 
                                                 (y :: r)
                                                 (DepElim.eq_simplification_sigma1
                                                 y1 y r9 r
                                                 (λ H2 : y1 = y,
                                                 DepElim.solution_left y
                                                 (λ (r10 : list B) 
                                                 (y4 : 
                                                 R n x y) 
                                                 (a2 : 
                                                 All2i R (S n) l r10) 
                                                 (H3 : 
                                                 r10 = r),
                                                 DepElim.solution_left r
                                                 (λ (y5 : R n x y) 
                                                 (a3 : 
                                                 All2i R (S n) l r),
                                                 {| pr1 := r0; pr2 := a |} =
                                                 {| pr1 := y5; pr2 := a3 |})
                                                 r10 H3 y4 a2) y1 H2 r9 y3 a1)))
                                                 l1 H1 r8 y2 a0) x H0 y l r
                                                 r7 b2)) eq_refl eq_refl,
                                             match
                                               H0 in (_ = s)
                                               return
                                                 (All2i_cons r0 a =
                                                 All2i_cons (pr1 s) (pr2 s))
                                             with
                                             | eq_refl => eq_refl
                                             end) 
                                          (All2i_cons r0 a) H) r5 e0 r6 b1)
                                y0 e'0 r3 r4 b0))) l0 e r1 r2 b) x e' y l r
              r0 a)) eq_refl eq_refl eq_refl eq_refl = eq_refl)


DEBUG:Going to execute:
simpl; DepElim.hnf_eq; DepElim.rewrite_refl_id