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
  ============================
   (let H := CoreTactics.block in
    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 r0 a0)
      (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 r0 a0) eq_refl) = eq_refl)


DEBUG:Going to execute:
intros _

Goals:
  
  A : Type
  B : Type
  R : A → B → Type
  R' : ∀ (a : A) (b : B), R a b → Type
  ============================
   (noConfusionHom_All2_dep_obligation_1 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 eq_refl) = eq_refl)

  
  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
  ============================
   (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 r0 a0)
      (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 r0 a0) eq_refl) = eq_refl)


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
  ============================
   (noConfusionHom_All2_dep_obligation_1 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 eq_refl) = eq_refl)

  
  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
  ============================
   (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 r0 a0)
      (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 r0 a0) eq_refl) = eq_refl)


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
  ============================
   (noConfusionHom_All2_dep_obligation_1 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 eq_refl) = eq_refl)

  
  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
  ============================
   (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 r0 a0)
      (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 r0 a0) eq_refl) = eq_refl)


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
  ============================
   (noConfusionHom_All2_dep_obligation_1 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 eq_refl) = eq_refl)

  
  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
  ============================
   (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 r0 a0)
      (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 r0 a0) eq_refl) = eq_refl)


DEBUG:Going to execute:
cbv zeta

Goals:
  
  A : Type
  B : Type
  R : A → B → Type
  R' : ∀ (a : A) (b : B), R a b → Type
  ============================
   (noConfusionHom_All2_dep_obligation_1 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 eq_refl) = eq_refl)

  
  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
  ============================
   (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 r0 a0)
      (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 r0 a0) eq_refl) = eq_refl)


DEBUG:Going to execute:
simpl
Level 2: evaluation returns
idtac of type tacvalue

Level 2: evaluation returns
idtac of type tacvalue


Goals:
  
  A : Type
  B : Type
  R : A → B → Type
  R' : ∀ (a : A) (b : B), R a b → Type
  ============================
   (apply_noConfusion [] []
      (Logic.True_rect_dep
         (λ H : True,
            ∀ e : 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 |},
              eq_rect
                {| pr1 := []; pr2 := {| pr1 := []; pr2 := All2_nil |} |}
                (λ index : sigma
                             (λ xs : list A,
                                sigma (λ ys : list B, All2 R xs ys)),
                   All2_dep R' (pr2 (pr2 index))) All2_dep_nil
                {| pr1 := []; pr2 := {| pr1 := []; pr2 := All2_nil |} |}
                (DepElim.pack_sigma_eq match H with
                                       | I => eq_refl
                                       end e) = All2_dep_nil
              → apply_noConfusion [] []
                  (Logic.True_rect_dep
                     (λ H0 : True,
                        eq_rect []
                          (λ xs : list A, sigma (λ ys : list B, All2 R xs ys))
                          {| pr1 := []; pr2 := All2_nil |} []
                          match H0 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
                              (λ H0 : True,
                                 eq_rect [] (λ ys : list B, All2 R [] ys)
                                   All2_nil []
                                   match H0 with
                                   | I => eq_refl
                                   end = All2_nil → Prop)
                              (apply_noConfusion All2_nil All2_nil
                                 (λ _ : True, True)))))) eq_refl eq_refl
                → All2_dep_nil = All2_dep_nil)
         (DepElim.eq_simplification_sigma1_dep_dep [] [] All2_nil All2_nil
            (apply_noConfusion [] []
               (Logic.True_rect_dep
                  (λ H : True,
                     ∀ e : eq_rect [] (λ ys : list B, All2 R [] ys) All2_nil
                             [] match H with
                                | I => eq_refl
                                end = All2_nil,
                       eq_rect
                         {|
                           pr1 := []; pr2 := {| pr1 := []; pr2 := All2_nil |}
                         |}
                         (λ index : sigma
                                      (λ xs : list A,
                                         sigma (λ ys : list B, All2 R xs ys)),
                            All2_dep R' (pr2 (pr2 index))) All2_dep_nil
                         {|
                           pr1 := []; pr2 := {| pr1 := []; pr2 := All2_nil |}
                         |}
                         match
                           DepElim.pack_sigma_eq
                             match H with
                             | I => eq_refl
                             end e in (_ = p)
                           return
                             ({|
                                pr1 := [];
                                pr2 := {| pr1 := []; pr2 := All2_nil |}
                              |} = {| pr1 := []; pr2 := p |})
                         with
                         | eq_refl => eq_refl
                         end = All2_dep_nil
                       → apply_noConfusion [] []
                           (Logic.True_rect_dep
                              (λ H0 : True,
                                 eq_rect []
                                   (λ xs : list A,
                                      sigma (λ ys : list B, All2 R xs ys))
                                   {| pr1 := []; pr2 := All2_nil |} []
                                   match H0 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
                                       (λ H0 : True,
                                          eq_rect []
                                            (λ ys : list B, All2 R [] ys)
                                            All2_nil []
                                            match H0 with
                                            | I => eq_refl
                                            end = All2_nil → Prop)
                                       (apply_noConfusion All2_nil All2_nil
                                          (λ _ : True, True)))))) eq_refl
                           eq_refl → All2_dep_nil = All2_dep_nil)
                  (apply_noConfusion All2_nil All2_nil
                     (Logic.True_rect_dep
                        (λ H : True,
                           eq_rect
                             {|
                               pr1 := [];
                               pr2 := {| pr1 := []; pr2 := All2_nil |}
                             |}
                             (λ index : sigma
                                          (λ xs : list A,
                                             sigma
                                               (λ ys : list B, All2 R xs ys)),
                                All2_dep R' (pr2 (pr2 index))) All2_dep_nil
                             {|
                               pr1 := [];
                               pr2 := {| pr1 := []; pr2 := All2_nil |}
                             |}
                             match
                               match
                                 apply_noConfusion [] []
                                   (Logic.True_rect_dep
                                      (λ H0 : True,
                                         ∀ e : [] = [],
                                           eq_rect 
                                             {| pr1 := []; pr2 := [] |}
                                             (λ index : 
                                                 sigma 
                                                 (λ _ : list A, list B),
                                                All2 R 
                                                 (pr1 index) 
                                                 (pr2 index)) All2_nil
                                             {| pr1 := []; pr2 := [] |}
                                             (DepElim.pack_sigma_eq_nondep
                                                match H0 with
                                                | I => eq_refl
                                                end e) = All2_nil
                                           → apply_noConfusion [] []
                                               (λ _ : True,
                                                 apply_noConfusion [] []
                                                 (λ _ : True, True)) eq_refl
                                               eq_refl → 
                                             All2_nil = All2_nil)
                                      (apply_noConfusion [] []
                                         (Logic.True_rect_dep
                                            (λ H0 : True,
                                               eq_rect
                                                 {| pr1 := []; pr2 := [] |}
                                                 (λ index : 
                                                 sigma 
                                                 (λ _ : list A, list B),
                                                 All2 R 
                                                 (pr1 index) 
                                                 (pr2 index)) All2_nil
                                                 {| pr1 := []; pr2 := [] |}
                                                 match
                                                 match H0 with
                                                 | I => eq_refl
                                                 end in 
                                                 (_ = p)
                                                 return
                                                 ({| pr1 := []; pr2 := [] |} =
                                                 {| pr1 := []; pr2 := p |})
                                                 with
                                                 | eq_refl => eq_refl
                                                 end = All2_nil
                                               → apply_noConfusion [] []
                                                 (λ _ : True,
                                                 apply_noConfusion [] []
                                                 (λ _ : True, True)) eq_refl
                                                 eq_refl
                                                 → 
                                                 All2_nil = All2_nil)
                                            (λ H0 : All2_nil = All2_nil,
                                               DepElim.solution_left All2_nil
                                                 (λ H1 : 
                                                 apply_noConfusion [] []
                                                 (λ _ : True,
                                                 apply_noConfusion [] []
                                                 (λ _ : True, True)) eq_refl
                                                 eq_refl,
                                                 match H1 with
                                                 | I => eq_refl
                                                 end) All2_nil H0)))) eq_refl
                                   eq_refl eq_refl H in 
                                 (_ = p)
                                 return
                                   ({| pr1 := []; pr2 := All2_nil |} =
                                    {| pr1 := []; pr2 := p |})
                               with
                               | eq_refl => eq_refl
                               end in (_ = p)
                               return
                                 ({|
                                    pr1 := [];
                                    pr2 := {| pr1 := []; pr2 := All2_nil |}
                                  |} = {| pr1 := []; pr2 := p |})
                             with
                             | eq_refl => eq_refl
                             end = All2_dep_nil
                           → apply_noConfusion [] []
                               (Logic.True_rect_dep
                                  (λ H0 : True,
                                     eq_rect []
                                       (λ xs : list A,
                                          sigma (λ ys : list B, All2 R xs ys))
                                       {| pr1 := []; pr2 := All2_nil |} []
                                       match H0 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
                                           (λ H0 : True,
                                              eq_rect []
                                                (λ ys : list B, All2 R [] ys)
                                                All2_nil []
                                                match H0 with
                                                | I => eq_refl
                                                end = All2_nil → Prop)
                                           (apply_noConfusion All2_nil
                                              All2_nil 
                                              (λ _ : True, True)))))) eq_refl
                               eq_refl → All2_dep_nil = All2_dep_nil)
                        (λ H : All2_dep_nil = All2_dep_nil,
                           DepElim.solution_left All2_dep_nil
                             (λ H0 : apply_noConfusion [] []
                                       (Logic.True_rect_dep
                                          (λ H0 : True,
                                             eq_rect []
                                               (λ xs : list A,
                                                 sigma
                                                 (λ ys : list B, All2 R xs ys))
                                               {|
                                                 pr1 := []; pr2 := All2_nil
                                               |} []
                                               match H0 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
                                                 (λ H0 : True,
                                                 eq_rect []
                                                 (λ ys : list B, All2 R [] ys)
                                                 All2_nil []
                                                 match H0 with
                                                 | I => eq_refl
                                                 end = All2_nil → Prop)
                                                 (apply_noConfusion All2_nil
                                                 All2_nil 
                                                 (λ _ : True, True))))))
                                       eq_refl eq_refl,
                                match H0 with
                                | I => eq_refl
                                end) All2_dep_nil H))))))) eq_refl eq_refl
      eq_refl I = eq_refl)

  
  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
  ============================
   (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) (l'0 : list B) 
                 (r1 : R x y0) (rs0 : All2 R l0 l'0) 
                 (r2 : R' x y0 r1) (b : All2_dep R' rs0) 
                 (e : l = l0),
                 DepElim.solution_right_dep l
                   (λ (l'1 : list B) (r3 : R x y0) 
                      (rs1 : All2 R l l'1) (r4 : R' x y0 r3) 
                      (b0 : All2_dep R' rs1),
                      DepElim.eq_simplification_sigma1_dep_dep 
                        (y :: l') (y0 :: l'1) (All2_cons r rs)
                        (All2_cons r3 rs1)
                        (apply_noConfusion (y :: l') 
                           (y0 :: l'1)
                           (DepElim.eq_simplification_sigma1_nondep_dep y y0
                              l' l'1
                              (λ e'0 : y = y0,
                                 DepElim.solution_right_dep y
                                   (λ (l'2 : list B) 
                                      (r5 : R x y) 
                                      (rs2 : All2 R l l'2) 
                                      (r6 : R' x y r5) 
                                      (b1 : All2_dep R' rs2) 
                                      (e0 : l' = l'2),
                                      DepElim.solution_right_dep l'
                                        (λ (r7 : R x y) 
                                           (rs3 : All2 R l l') 
                                           (r8 : R' x y r7) 
                                           (b2 : All2_dep R' rs3),
                                           apply_noConfusion 
                                             (All2_cons r rs)
                                             (All2_cons r7 rs3)
                                             (DepElim.eq_simplification_sigma1_nondep_dep
                                                r r7 rs rs3
                                                (λ e'1 : r = r7,
                                                 DepElim.solution_right_dep r
                                                 (λ (rs4 : All2 R l l') 
                                                 (r9 : 
                                                 R' x y r) 
                                                 (b3 : 
                                                 All2_dep R' rs4) 
                                                 (e1 : 
                                                 rs = rs4),
                                                 DepElim.solution_right_dep
                                                 rs
                                                 (λ (r10 : R' x y r) 
                                                 (b4 : 
                                                 All2_dep R' rs) 
                                                 (H : 
                                                 All2_dep_cons r0 a0 =
                                                 All2_dep_cons r10 b4),
                                                 DepElim.solution_left
                                                 (All2_dep_cons r10 b4)
                                                 (λ H0 : 
                                                 apply_noConfusion 
                                                 (x :: l) 
                                                 (x :: l)
                                                 (DepElim.eq_simplification_sigma1_nondep_dep
                                                 x x l l
                                                 (λ e'2 : x = x,
                                                 DepElim.solution_left_dep x
                                                 (λ (y1 : B) 
                                                 (l1 : list A) 
                                                 (l'3 : list B) 
                                                 (r11 : 
                                                 R x y1) 
                                                 (rs5 : 
                                                 All2 R l1 l'3) 
                                                 (y2 : 
                                                 R' x y1 r11) 
                                                 (a : 
                                                 All2_dep R' rs5) 
                                                 (e2 : 
                                                 l1 = l),
                                                 DepElim.solution_left_dep l
                                                 (λ (l'4 : list B) 
                                                 (r12 : 
                                                 R x y1) 
                                                 (rs6 : All2 R l l'4) 
                                                 (y3 : 
                                                 R' x y1 r12) 
                                                 (a1 : 
                                                 All2_dep R' rs6),
                                                 DepElim.eq_simplification_sigma1_dep
                                                 (y1 :: l'4) 
                                                 (y :: l')
                                                 (All2_cons r12 rs6)
                                                 (All2_cons r rs)
                                                 (apply_noConfusion
                                                 (y1 :: l'4) 
                                                 (y :: l')
                                                 (DepElim.eq_simplification_sigma1_nondep_dep
                                                 y1 y l'4 l'
                                                 (λ e'3 : y1 = y,
                                                 DepElim.solution_left_dep y
                                                 (λ (l'5 : list B) 
                                                 (r13 : 
                                                 R x y) 
                                                 (rs7 : All2 R l l'5) 
                                                 (y4 : 
                                                 R' x y r13) 
                                                 (a2 : 
                                                 All2_dep R' rs7) 
                                                 (e3 : 
                                                 l'5 = l'),
                                                 DepElim.solution_left_dep l'
                                                 (λ (r14 : R x y) 
                                                 (rs8 : 
                                                 All2 R l l') 
                                                 (y5 : 
                                                 R' x y r14) 
                                                 (a3 : 
                                                 All2_dep R' rs8),
                                                 apply_noConfusion
                                                 (All2_cons r14 rs8)
                                                 (All2_cons r rs)
                                                 (DepElim.eq_simplification_sigma1
                                                 r14 r rs8 rs
                                                 (λ H0 : r14 = r,
                                                 DepElim.solution_left r
                                                 (λ (rs9 : All2 R l l') 
                                                 (y6 : 
                                                 R' x y r) 
                                                 (a4 : 
                                                 All2_dep R' rs9) 
                                                 (H1 : 
                                                 rs9 = rs),
                                                 DepElim.solution_left rs
                                                 (λ (y7 : R' x y r) 
                                                 (a5 : 
                                                 All2_dep R' rs),
                                                 {| pr1 := r0; pr2 := a0 |} =
                                                 {| pr1 := y7; pr2 := a5 |})
                                                 rs9 H1 y6 a4) r14 H0 rs8 y5
                                                 a3))) l'5 e3 r13 rs7 y4 a2)
                                                 y1 e'3 l'4 r12 rs6 y3 a1))))
                                                 l1 e2 l'3 r11 rs5 y2 a) x
                                                 e'2 y l l' r rs r10 b4))
                                                 eq_refl eq_refl,
                                                 match
                                                 H0 in (_ = s)
                                                 return
                                                 (All2_dep_cons r0 a0 =
                                                 All2_dep_cons 
                                                 (pr1 s) 
                                                 (pr2 s))
                                                 with
                                                 | eq_refl => eq_refl
                                                 end) 
                                                 (All2_dep_cons r0 a0) H) rs4
                                                 e1 r9 b3) r7 e'1 rs3 r8 b2)))
                                        l'2 e0 r5 rs2 r6 b1) y0 e'0 l'1 r3
                                   rs1 r4 b0)))) l0 e l'0 r1 rs0 r2 b) x e' y
              l l' r rs r0 a0)) eq_refl eq_refl eq_refl eq_refl = eq_refl)


DEBUG:Going to execute:
DepElim.simpl_equations

Goals:
  
  A : Type
  B : Type
  R : A → B → Type
  R' : ∀ (a : A) (b : B), R a b → Type
  ============================
   (apply_noConfusion [] []
      (Logic.True_rect_dep
         (λ H : True,
            ∀ e : 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 |},
              eq_rect
                {| pr1 := []; pr2 := {| pr1 := []; pr2 := All2_nil |} |}
                (λ index : sigma
                             (λ xs : list A,
                                sigma (λ ys : list B, All2 R xs ys)),
                   All2_dep R' (pr2 (pr2 index))) All2_dep_nil
                {| pr1 := []; pr2 := {| pr1 := []; pr2 := All2_nil |} |}
                (DepElim.pack_sigma_eq match H with
                                       | I => eq_refl
                                       end e) = All2_dep_nil
              → apply_noConfusion [] []
                  (Logic.True_rect_dep
                     (λ H0 : True,
                        eq_rect []
                          (λ xs : list A, sigma (λ ys : list B, All2 R xs ys))
                          {| pr1 := []; pr2 := All2_nil |} []
                          match H0 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
                              (λ H0 : True,
                                 eq_rect [] (λ ys : list B, All2 R [] ys)
                                   All2_nil []
                                   match H0 with
                                   | I => eq_refl
                                   end = All2_nil → Prop)
                              (apply_noConfusion All2_nil All2_nil
                                 (λ _ : True, True)))))) eq_refl eq_refl
                → All2_dep_nil = All2_dep_nil)
         (DepElim.eq_simplification_sigma1_dep_dep [] [] All2_nil All2_nil
            (apply_noConfusion [] []
               (Logic.True_rect_dep
                  (λ H : True,
                     ∀ e : eq_rect [] (λ ys : list B, All2 R [] ys) All2_nil
                             [] match H with
                                | I => eq_refl
                                end = All2_nil,
                       eq_rect
                         {|
                           pr1 := []; pr2 := {| pr1 := []; pr2 := All2_nil |}
                         |}
                         (λ index : sigma
                                      (λ xs : list A,
                                         sigma (λ ys : list B, All2 R xs ys)),
                            All2_dep R' (pr2 (pr2 index))) All2_dep_nil
                         {|
                           pr1 := []; pr2 := {| pr1 := []; pr2 := All2_nil |}
                         |}
                         match
                           DepElim.pack_sigma_eq
                             match H with
                             | I => eq_refl
                             end e in (_ = p)
                           return
                             ({|
                                pr1 := [];
                                pr2 := {| pr1 := []; pr2 := All2_nil |}
                              |} = {| pr1 := []; pr2 := p |})
                         with
                         | eq_refl => eq_refl
                         end = All2_dep_nil
                       → apply_noConfusion [] []
                           (Logic.True_rect_dep
                              (λ H0 : True,
                                 eq_rect []
                                   (λ xs : list A,
                                      sigma (λ ys : list B, All2 R xs ys))
                                   {| pr1 := []; pr2 := All2_nil |} []
                                   match H0 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
                                       (λ H0 : True,
                                          eq_rect []
                                            (λ ys : list B, All2 R [] ys)
                                            All2_nil []
                                            match H0 with
                                            | I => eq_refl
                                            end = All2_nil → Prop)
                                       (apply_noConfusion All2_nil All2_nil
                                          (λ _ : True, True)))))) eq_refl
                           eq_refl → All2_dep_nil = All2_dep_nil)
                  (apply_noConfusion All2_nil All2_nil
                     (Logic.True_rect_dep
                        (λ H : True,
                           eq_rect
                             {|
                               pr1 := [];
                               pr2 := {| pr1 := []; pr2 := All2_nil |}
                             |}
                             (λ index : sigma
                                          (λ xs : list A,
                                             sigma
                                               (λ ys : list B, All2 R xs ys)),
                                All2_dep R' (pr2 (pr2 index))) All2_dep_nil
                             {|
                               pr1 := [];
                               pr2 := {| pr1 := []; pr2 := All2_nil |}
                             |}
                             match
                               match
                                 apply_noConfusion [] []
                                   (Logic.True_rect_dep
                                      (λ H0 : True,
                                         ∀ e : [] = [],
                                           eq_rect 
                                             {| pr1 := []; pr2 := [] |}
                                             (λ index : 
                                                 sigma 
                                                 (λ _ : list A, list B),
                                                All2 R 
                                                 (pr1 index) 
                                                 (pr2 index)) All2_nil
                                             {| pr1 := []; pr2 := [] |}
                                             (DepElim.pack_sigma_eq_nondep
                                                match H0 with
                                                | I => eq_refl
                                                end e) = All2_nil
                                           → apply_noConfusion [] []
                                               (λ _ : True,
                                                 apply_noConfusion [] []
                                                 (λ _ : True, True)) eq_refl
                                               eq_refl → 
                                             All2_nil = All2_nil)
                                      (apply_noConfusion [] []
                                         (Logic.True_rect_dep
                                            (λ H0 : True,
                                               eq_rect
                                                 {| pr1 := []; pr2 := [] |}
                                                 (λ index : 
                                                 sigma 
                                                 (λ _ : list A, list B),
                                                 All2 R 
                                                 (pr1 index) 
                                                 (pr2 index)) All2_nil
                                                 {| pr1 := []; pr2 := [] |}
                                                 match
                                                 match H0 with
                                                 | I => eq_refl
                                                 end in 
                                                 (_ = p)
                                                 return
                                                 ({| pr1 := []; pr2 := [] |} =
                                                 {| pr1 := []; pr2 := p |})
                                                 with
                                                 | eq_refl => eq_refl
                                                 end = All2_nil
                                               → apply_noConfusion [] []
                                                 (λ _ : True,
                                                 apply_noConfusion [] []
                                                 (λ _ : True, True)) eq_refl
                                                 eq_refl
                                                 → 
                                                 All2_nil = All2_nil)
                                            (λ H0 : All2_nil = All2_nil,
                                               DepElim.solution_left All2_nil
                                                 (λ H1 : 
                                                 apply_noConfusion [] []
                                                 (λ _ : True,
                                                 apply_noConfusion [] []
                                                 (λ _ : True, True)) eq_refl
                                                 eq_refl,
                                                 match H1 with
                                                 | I => eq_refl
                                                 end) All2_nil H0)))) eq_refl
                                   eq_refl eq_refl H in 
                                 (_ = p)
                                 return
                                   ({| pr1 := []; pr2 := All2_nil |} =
                                    {| pr1 := []; pr2 := p |})
                               with
                               | eq_refl => eq_refl
                               end in (_ = p)
                               return
                                 ({|
                                    pr1 := [];
                                    pr2 := {| pr1 := []; pr2 := All2_nil |}
                                  |} = {| pr1 := []; pr2 := p |})
                             with
                             | eq_refl => eq_refl
                             end = All2_dep_nil
                           → apply_noConfusion [] []
                               (Logic.True_rect_dep
                                  (λ H0 : True,
                                     eq_rect []
                                       (λ xs : list A,
                                          sigma (λ ys : list B, All2 R xs ys))
                                       {| pr1 := []; pr2 := All2_nil |} []
                                       match H0 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
                                           (λ H0 : True,
                                              eq_rect []
                                                (λ ys : list B, All2 R [] ys)
                                                All2_nil []
                                                match H0 with
                                                | I => eq_refl
                                                end = All2_nil → Prop)
                                           (apply_noConfusion All2_nil
                                              All2_nil 
                                              (λ _ : True, True)))))) eq_refl
                               eq_refl → All2_dep_nil = All2_dep_nil)
                        (λ H : All2_dep_nil = All2_dep_nil,
                           DepElim.solution_left All2_dep_nil
                             (λ H0 : apply_noConfusion [] []
                                       (Logic.True_rect_dep
                                          (λ H0 : True,
                                             eq_rect []
                                               (λ xs : list A,
                                                 sigma
                                                 (λ ys : list B, All2 R xs ys))
                                               {|
                                                 pr1 := []; pr2 := All2_nil
                                               |} []
                                               match H0 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
                                                 (λ H0 : True,
                                                 eq_rect []
                                                 (λ ys : list B, All2 R [] ys)
                                                 All2_nil []
                                                 match H0 with
                                                 | I => eq_refl
                                                 end = All2_nil → Prop)
                                                 (apply_noConfusion All2_nil
                                                 All2_nil 
                                                 (λ _ : True, True))))))
                                       eq_refl eq_refl,
                                match H0 with
                                | I => eq_refl
                                end) All2_dep_nil H))))))) eq_refl eq_refl
      eq_refl I = eq_refl)

  
  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
  ============================
   (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) (l'0 : list B) 
                 (r1 : R x y0) (rs0 : All2 R l0 l'0) 
                 (r2 : R' x y0 r1) (b : All2_dep R' rs0) 
                 (e : l = l0),
                 DepElim.solution_right_dep l
                   (λ (l'1 : list B) (r3 : R x y0) 
                      (rs1 : All2 R l l'1) (r4 : R' x y0 r3) 
                      (b0 : All2_dep R' rs1),
                      DepElim.eq_simplification_sigma1_dep_dep 
                        (y :: l') (y0 :: l'1) (All2_cons r rs)
                        (All2_cons r3 rs1)
                        (apply_noConfusion (y :: l') 
                           (y0 :: l'1)
                           (DepElim.eq_simplification_sigma1_nondep_dep y y0
                              l' l'1
                              (λ e'0 : y = y0,
                                 DepElim.solution_right_dep y
                                   (λ (l'2 : list B) 
                                      (r5 : R x y) 
                                      (rs2 : All2 R l l'2) 
                                      (r6 : R' x y r5) 
                                      (b1 : All2_dep R' rs2) 
                                      (e0 : l' = l'2),
                                      DepElim.solution_right_dep l'
                                        (λ (r7 : R x y) 
                                           (rs3 : All2 R l l') 
                                           (r8 : R' x y r7) 
                                           (b2 : All2_dep R' rs3),
                                           apply_noConfusion 
                                             (All2_cons r rs)
                                             (All2_cons r7 rs3)
                                             (DepElim.eq_simplification_sigma1_nondep_dep
                                                r r7 rs rs3
                                                (λ e'1 : r = r7,
                                                 DepElim.solution_right_dep r
                                                 (λ (rs4 : All2 R l l') 
                                                 (r9 : 
                                                 R' x y r) 
                                                 (b3 : 
                                                 All2_dep R' rs4) 
                                                 (e1 : 
                                                 rs = rs4),
                                                 DepElim.solution_right_dep
                                                 rs
                                                 (λ (r10 : R' x y r) 
                                                 (b4 : 
                                                 All2_dep R' rs) 
                                                 (H : 
                                                 All2_dep_cons r0 a0 =
                                                 All2_dep_cons r10 b4),
                                                 DepElim.solution_left
                                                 (All2_dep_cons r10 b4)
                                                 (λ H0 : 
                                                 apply_noConfusion 
                                                 (x :: l) 
                                                 (x :: l)
                                                 (DepElim.eq_simplification_sigma1_nondep_dep
                                                 x x l l
                                                 (λ e'2 : x = x,
                                                 DepElim.solution_left_dep x
                                                 (λ (y1 : B) 
                                                 (l1 : list A) 
                                                 (l'3 : list B) 
                                                 (r11 : 
                                                 R x y1) 
                                                 (rs5 : 
                                                 All2 R l1 l'3) 
                                                 (y2 : 
                                                 R' x y1 r11) 
                                                 (a : 
                                                 All2_dep R' rs5) 
                                                 (e2 : 
                                                 l1 = l),
                                                 DepElim.solution_left_dep l
                                                 (λ (l'4 : list B) 
                                                 (r12 : 
                                                 R x y1) 
                                                 (rs6 : All2 R l l'4) 
                                                 (y3 : 
                                                 R' x y1 r12) 
                                                 (a1 : 
                                                 All2_dep R' rs6),
                                                 DepElim.eq_simplification_sigma1_dep
                                                 (y1 :: l'4) 
                                                 (y :: l')
                                                 (All2_cons r12 rs6)
                                                 (All2_cons r rs)
                                                 (apply_noConfusion
                                                 (y1 :: l'4) 
                                                 (y :: l')
                                                 (DepElim.eq_simplification_sigma1_nondep_dep
                                                 y1 y l'4 l'
                                                 (λ e'3 : y1 = y,
                                                 DepElim.solution_left_dep y
                                                 (λ (l'5 : list B) 
                                                 (r13 : 
                                                 R x y) 
                                                 (rs7 : All2 R l l'5) 
                                                 (y4 : 
                                                 R' x y r13) 
                                                 (a2 : 
                                                 All2_dep R' rs7) 
                                                 (e3 : 
                                                 l'5 = l'),
                                                 DepElim.solution_left_dep l'
                                                 (λ (r14 : R x y) 
                                                 (rs8 : 
                                                 All2 R l l') 
                                                 (y5 : 
                                                 R' x y r14) 
                                                 (a3 : 
                                                 All2_dep R' rs8),
                                                 apply_noConfusion
                                                 (All2_cons r14 rs8)
                                                 (All2_cons r rs)
                                                 (DepElim.eq_simplification_sigma1
                                                 r14 r rs8 rs
                                                 (λ H0 : r14 = r,
                                                 DepElim.solution_left r
                                                 (λ (rs9 : All2 R l l') 
                                                 (y6 : 
                                                 R' x y r) 
                                                 (a4 : 
                                                 All2_dep R' rs9) 
                                                 (H1 : 
                                                 rs9 = rs),
                                                 DepElim.solution_left rs
                                                 (λ (y7 : R' x y r) 
                                                 (a5 : 
                                                 All2_dep R' rs),
                                                 {| pr1 := r0; pr2 := a0 |} =
                                                 {| pr1 := y7; pr2 := a5 |})
                                                 rs9 H1 y6 a4) r14 H0 rs8 y5
                                                 a3))) l'5 e3 r13 rs7 y4 a2)
                                                 y1 e'3 l'4 r12 rs6 y3 a1))))
                                                 l1 e2 l'3 r11 rs5 y2 a) x
                                                 e'2 y l l' r rs r10 b4))
                                                 eq_refl eq_refl,
                                                 match
                                                 H0 in (_ = s)
                                                 return
                                                 (All2_dep_cons r0 a0 =
                                                 All2_dep_cons 
                                                 (pr1 s) 
                                                 (pr2 s))
                                                 with
                                                 | eq_refl => eq_refl
                                                 end) 
                                                 (All2_dep_cons r0 a0) H) rs4
                                                 e1 r9 b3) r7 e'1 rs3 r8 b2)))
                                        l'2 e0 r5 rs2 r6 b1) y0 e'0 l'1 r3
                                   rs1 r4 b0)))) l0 e l'0 r1 rs0 r2 b) x e' y
              l l' r rs r0 a0)) eq_refl eq_refl eq_refl eq_refl = eq_refl)


DEBUG:Going to execute:
repeat
            (repeat (simpl; DepElim.hnf_eq; DepElim.rewrite_refl_id);
              try progress autounfold with equations)