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
  e : NoConfusionHom_All2_dep A B R R' (x :: l) (y :: l') 
        (All2_cons r rs) (All2_dep_cons r0 a0) (All2_dep_cons r2 b)
  ============================
   (let H := CoreTactics.block in
    noConfusionHom_All2_dep_obligation_2 A B R R' 
      (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0)
      (All2_dep_cons r2 b)
      (noConfusionHom_All2_dep_obligation_1 A B R R' 
         (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0)
         (All2_dep_cons r2 b) e) = e)


DEBUG:Going to execute:
intros _

Goals:
  
  A : Type
  B : Type
  R : A → B → Type
  R' : ∀ (a : A) (b : B), R a b → Type
  e : NoConfusionHom_All2_dep A B R R' [] [] All2_nil All2_dep_nil
        All2_dep_nil
  ============================
   (noConfusionHom_All2_dep_obligation_2 A B R R' [] [] All2_nil All2_dep_nil
      All2_dep_nil
      (noConfusionHom_All2_dep_obligation_1 A B R R' [] [] All2_nil
         All2_dep_nil All2_dep_nil e) = e)

  
  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
  e : NoConfusionHom_All2_dep A B R R' (x :: l) (y :: l') 
        (All2_cons r rs) (All2_dep_cons r0 a0) (All2_dep_cons r2 b)
  ============================
   (noConfusionHom_All2_dep_obligation_2 A B R R' 
      (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0)
      (All2_dep_cons r2 b)
      (noConfusionHom_All2_dep_obligation_1 A B R R' 
         (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0)
         (All2_dep_cons r2 b) e) = e)


DEBUG:Going to execute:
CoreTactics.unblock_goal

Goals:
  
  A : Type
  B : Type
  R : A → B → Type
  R' : ∀ (a : A) (b : B), R a b → Type
  e : NoConfusionHom_All2_dep A B R R' [] [] All2_nil All2_dep_nil
        All2_dep_nil
  ============================
   (noConfusionHom_All2_dep_obligation_2 A B R R' [] [] All2_nil All2_dep_nil
      All2_dep_nil
      (noConfusionHom_All2_dep_obligation_1 A B R R' [] [] All2_nil
         All2_dep_nil All2_dep_nil e) = e)

  
  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
  e : NoConfusionHom_All2_dep A B R R' (x :: l) (y :: l') 
        (All2_cons r rs) (All2_dep_cons r0 a0) (All2_dep_cons r2 b)
  ============================
   (noConfusionHom_All2_dep_obligation_2 A B R R' 
      (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0)
      (All2_dep_cons r2 b)
      (noConfusionHom_All2_dep_obligation_1 A B R R' 
         (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0)
         (All2_dep_cons r2 b) e) = e)


DEBUG:Going to execute:
unfold CoreTactics.block in *; cbv zeta

Goals:
  
  A : Type
  B : Type
  R : A → B → Type
  R' : ∀ (a : A) (b : B), R a b → Type
  e : NoConfusionHom_All2_dep A B R R' [] [] All2_nil All2_dep_nil
        All2_dep_nil
  ============================
   (noConfusionHom_All2_dep_obligation_2 A B R R' [] [] All2_nil All2_dep_nil
      All2_dep_nil
      (noConfusionHom_All2_dep_obligation_1 A B R R' [] [] All2_nil
         All2_dep_nil All2_dep_nil e) = e)

  
  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
  e : NoConfusionHom_All2_dep A B R R' (x :: l) (y :: l') 
        (All2_cons r rs) (All2_dep_cons r0 a0) (All2_dep_cons r2 b)
  ============================
   (noConfusionHom_All2_dep_obligation_2 A B R R' 
      (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0)
      (All2_dep_cons r2 b)
      (noConfusionHom_All2_dep_obligation_1 A B R R' 
         (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0)
         (All2_dep_cons r2 b) e) = e)


DEBUG:Going to execute:
unfold CoreTactics.block in *

Goals:
  
  A : Type
  B : Type
  R : A → B → Type
  R' : ∀ (a : A) (b : B), R a b → Type
  e : NoConfusionHom_All2_dep A B R R' [] [] All2_nil All2_dep_nil
        All2_dep_nil
  ============================
   (noConfusionHom_All2_dep_obligation_2 A B R R' [] [] All2_nil All2_dep_nil
      All2_dep_nil
      (noConfusionHom_All2_dep_obligation_1 A B R R' [] [] All2_nil
         All2_dep_nil All2_dep_nil e) = e)

  
  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
  e : NoConfusionHom_All2_dep A B R R' (x :: l) (y :: l') 
        (All2_cons r rs) (All2_dep_cons r0 a0) (All2_dep_cons r2 b)
  ============================
   (noConfusionHom_All2_dep_obligation_2 A B R R' 
      (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0)
      (All2_dep_cons r2 b)
      (noConfusionHom_All2_dep_obligation_1 A B R R' 
         (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0)
         (All2_dep_cons r2 b) e) = e)


DEBUG:Going to execute:
cbv zeta

Goals:
  
  A : Type
  B : Type
  R : A → B → Type
  R' : ∀ (a : A) (b : B), R a b → Type
  e : NoConfusionHom_All2_dep A B R R' [] [] All2_nil All2_dep_nil
        All2_dep_nil
  ============================
   (noConfusionHom_All2_dep_obligation_2 A B R R' [] [] All2_nil All2_dep_nil
      All2_dep_nil
      (noConfusionHom_All2_dep_obligation_1 A B R R' [] [] All2_nil
         All2_dep_nil All2_dep_nil e) = e)

  
  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
  e : NoConfusionHom_All2_dep A B R R' (x :: l) (y :: l') 
        (All2_cons r rs) (All2_dep_cons r0 a0) (All2_dep_cons r2 b)
  ============================
   (noConfusionHom_All2_dep_obligation_2 A B R R' 
      (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0)
      (All2_dep_cons r2 b)
      (noConfusionHom_All2_dep_obligation_1 A B R R' 
         (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0)
         (All2_dep_cons r2 b) e) = e)


DEBUG:Going to execute:
simpl in * |-

Goals:
  
  A : Type
  B : Type
  R : A → B → Type
  R' : ∀ (a : A) (b : B), R a b → Type
  e : apply_noConfusion [] []
        (Logic.True_rect_dep
           (λ H : True,
              eq_rect [] (λ xs : list A, sigma (λ ys : list B, All2 R xs ys))
                {| pr1 := []; pr2 := All2_nil |} []
                match H with
                | I => eq_refl
                end = {| pr1 := []; pr2 := All2_nil |} → Prop)
           (DepElim.eq_simplification_sigma1_dep [] [] All2_nil All2_nil
              (apply_noConfusion [] []
                 (Logic.True_rect_dep
                    (λ H : True,
                       eq_rect [] (λ ys : list B, All2 R [] ys) All2_nil []
                         match H with
                         | I => eq_refl
                         end = All2_nil → Prop)
                    (apply_noConfusion All2_nil All2_nil (λ _ : True, True))))))
        eq_refl eq_refl
  ============================
   (noConfusionHom_All2_dep_obligation_2 A B R R' [] [] All2_nil All2_dep_nil
      All2_dep_nil
      (noConfusionHom_All2_dep_obligation_1 A B R R' [] [] All2_nil
         All2_dep_nil All2_dep_nil e) = e)

  
  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
  e : 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
  ============================
   (noConfusionHom_All2_dep_obligation_2 A B R R' 
      (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0)
      (All2_dep_cons r2 b)
      (noConfusionHom_All2_dep_obligation_1 A B R R' 
         (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0)
         (All2_dep_cons r2 b) e) = e)


DEBUG:Going to execute:
CoreTactics.on_last_hyp
            ltac:(fun id =>
                    hnf in id;
                     CoreTactics.destruct_tele_eq id || DepElim.depelim id)

Goals:
  
  A : Type
  B : Type
  R : A → B → Type
  R' : ∀ (a : A) (b : B), R a b → Type
  e : apply_noConfusion [] []
        (Logic.True_rect_dep
           (λ H : True,
              eq_rect [] (λ xs : list A, sigma (λ ys : list B, All2 R xs ys))
                {| pr1 := []; pr2 := All2_nil |} []
                match H with
                | I => eq_refl
                end = {| pr1 := []; pr2 := All2_nil |} → Prop)
           (DepElim.eq_simplification_sigma1_dep [] [] All2_nil All2_nil
              (apply_noConfusion [] []
                 (Logic.True_rect_dep
                    (λ H : True,
                       eq_rect [] (λ ys : list B, All2 R [] ys) All2_nil []
                         match H with
                         | I => eq_refl
                         end = All2_nil → Prop)
                    (apply_noConfusion All2_nil All2_nil (λ _ : True, True))))))
        eq_refl eq_refl
  ============================
   (noConfusionHom_All2_dep_obligation_2 A B R R' [] [] All2_nil All2_dep_nil
      All2_dep_nil
      (noConfusionHom_All2_dep_obligation_1 A B R R' [] [] All2_nil
         All2_dep_nil All2_dep_nil e) = e)

  
  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
  e : 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
  ============================
   (noConfusionHom_All2_dep_obligation_2 A B R R' 
      (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0)
      (All2_dep_cons r2 b)
      (noConfusionHom_All2_dep_obligation_1 A B R R' 
         (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0)
         (All2_dep_cons r2 b) e) = e)


DEBUG:Going to execute:
fun tac => lazymatch goal with
                      | H:_ |- _ => tac H
                      end

Goals:
  
  A : Type
  B : Type
  R : A → B → Type
  R' : ∀ (a : A) (b : B), R a b → Type
  e : apply_noConfusion [] []
        (Logic.True_rect_dep
           (λ H : True,
              eq_rect [] (λ xs : list A, sigma (λ ys : list B, All2 R xs ys))
                {| pr1 := []; pr2 := All2_nil |} []
                match H with
                | I => eq_refl
                end = {| pr1 := []; pr2 := All2_nil |} → Prop)
           (DepElim.eq_simplification_sigma1_dep [] [] All2_nil All2_nil
              (apply_noConfusion [] []
                 (Logic.True_rect_dep
                    (λ H : True,
                       eq_rect [] (λ ys : list B, All2 R [] ys) All2_nil []
                         match H with
                         | I => eq_refl
                         end = All2_nil → Prop)
                    (apply_noConfusion All2_nil All2_nil (λ _ : True, True))))))
        eq_refl eq_refl
  ============================
   (noConfusionHom_All2_dep_obligation_2 A B R R' [] [] All2_nil All2_dep_nil
      All2_dep_nil
      (noConfusionHom_All2_dep_obligation_1 A B R R' [] [] All2_nil
         All2_dep_nil All2_dep_nil e) = e)

  
  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
  e : 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
  ============================
   (noConfusionHom_All2_dep_obligation_2 A B R R' 
      (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0)
      (All2_dep_cons r2 b)
      (noConfusionHom_All2_dep_obligation_1 A B R R' 
         (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0)
         (All2_dep_cons r2 b) e) = e)


DEBUG:Going to execute:
fun id =>
             hnf in id; CoreTactics.destruct_tele_eq id || DepElim.depelim id

Goals:
  
  A : Type
  B : Type
  R : A → B → Type
  R' : ∀ (a : A) (b : B), R a b → Type
  e : apply_noConfusion [] []
        (Logic.True_rect_dep
           (λ H : True,
              eq_rect [] (λ xs : list A, sigma (λ ys : list B, All2 R xs ys))
                {| pr1 := []; pr2 := All2_nil |} []
                match H with
                | I => eq_refl
                end = {| pr1 := []; pr2 := All2_nil |} → Prop)
           (DepElim.eq_simplification_sigma1_dep [] [] All2_nil All2_nil
              (apply_noConfusion [] []
                 (Logic.True_rect_dep
                    (λ H : True,
                       eq_rect [] (λ ys : list B, All2 R [] ys) All2_nil []
                         match H with
                         | I => eq_refl
                         end = All2_nil → Prop)
                    (apply_noConfusion All2_nil All2_nil (λ _ : True, True))))))
        eq_refl eq_refl
  ============================
   (noConfusionHom_All2_dep_obligation_2 A B R R' [] [] All2_nil All2_dep_nil
      All2_dep_nil
      (noConfusionHom_All2_dep_obligation_1 A B R R' [] [] All2_nil
         All2_dep_nil All2_dep_nil e) = e)

  
  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
  e : 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
  ============================
   (noConfusionHom_All2_dep_obligation_2 A B R R' 
      (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0)
      (All2_dep_cons r2 b)
      (noConfusionHom_All2_dep_obligation_1 A B R R' 
         (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0)
         (All2_dep_cons r2 b) e) = e)


DEBUG:Going to execute:
lazymatch goal with
           | H:_ |- _ => tac H
           end