Goal:
  
  A : Type
  B : Type
  R : A → B → Type
  R' : ∀ (a : A) (b : B), R a b → Type
  x : A
  y : B
  l : list A
  l' : list B
  r : R x y
  rs : All2 R l l'
  r0 : R' x y r
  a0 : All2_dep R' rs
  r2 : R' x y r
  b : All2_dep R' rs
  H : apply_noConfusion (x :: l) (x :: l)
        (DepElim.eq_simplification_sigma1_nondep_dep x x l l
           (λ e' : x = x,
              DepElim.solution_left_dep x
                (λ (y0 : B) (l0 : list A) (l'0 : list B) 
                   (r1 : R x y0) (rs0 : All2 R l0 l'0) 
                   (y1 : R' x y0 r1) (a : All2_dep R' rs0) 
                   (e : l0 = l),
                   DepElim.solution_left_dep l
                     (λ (l'1 : list B) (r2 : R x y0) 
                        (rs1 : All2 R l l'1) (y2 : R' x y0 r2) 
                        (a1 : All2_dep R' rs1),
                        DepElim.eq_simplification_sigma1_dep 
                          (y0 :: l'1) (y :: l') (All2_cons r2 rs1)
                          (All2_cons r rs)
                          (apply_noConfusion (y0 :: l'1) 
                             (y :: l')
                             (DepElim.eq_simplification_sigma1_nondep_dep y0
                                y l'1 l'
                                (λ e'0 : y0 = y,
                                   DepElim.solution_left_dep y
                                     (λ (l'2 : list B) 
                                        (r3 : R x y) 
                                        (rs2 : All2 R l l'2) 
                                        (y3 : R' x y r3) 
                                        (a2 : All2_dep R' rs2) 
                                        (e0 : l'2 = l'),
                                        DepElim.solution_left_dep l'
                                          (λ (r4 : R x y) 
                                             (rs3 : All2 R l l') 
                                             (y4 : 
                                              R' x y r4) 
                                             (a3 : 
                                              All2_dep R' rs3),
                                             apply_noConfusion
                                               (All2_cons r4 rs3)
                                               (All2_cons r rs)
                                               (DepElim.eq_simplification_sigma1
                                                 r4 r rs3 rs
                                                 (λ H : r4 = r,
                                                 DepElim.solution_left r
                                                 (λ (rs4 : All2 R l l') 
                                                 (y5 : 
                                                 R' x y r) 
                                                 (a4 : 
                                                 All2_dep R' rs4) 
                                                 (H0 : 
                                                 rs4 = rs),
                                                 DepElim.solution_left rs
                                                 (λ (y6 : R' x y r) 
                                                 (a5 : 
                                                 All2_dep R' rs),
                                                 {| pr1 := r0; pr2 := a0 |} =
                                                 {| pr1 := y6; pr2 := a5 |})
                                                 rs4 H0 y5 a4) r4 H rs3 y4 a3)))
                                          l'2 e0 r3 rs2 y3 a2) y0 e'0 l'1 r2
                                     rs1 y2 a1)))) l0 e l'0 r1 rs0 y1 a) x e'
                y l l' r rs r2 b)) eq_refl eq_refl
  ============================
   (All2_dep_cons r0 a0 = All2_dep_cons r2 b)


DEBUG:Going to execute:
tac H