Goal:
  
  A : Type
  B : Type
  C : Type
  R : A → B → C → Type
  x : A
  y : B
  z : C
  l : list A
  l' : list B
  l'' : list C
  r : R x y z
  a : All3 R l l' l''
  ============================
   (let H := CoreTactics.block in
    noConfusionHom_All3_obligation_1 A B C R (x :: l) 
      (y :: l') (z :: l'') (All3_cons r a) (All3_cons r a)
      (noConfusionHom_All3_obligation_2 A B C R (x :: l) 
         (y :: l') (z :: l'') (All3_cons r a) (All3_cons r a) eq_refl) =
    eq_refl)


DEBUG:Going to execute:
intros _

Goals:
    A : Type  B : Type  C : Type  R : A → B → C → Type
  ============================
   (noConfusionHom_All3_obligation_1 A B C R [] [] [] All3_nil All3_nil
      (noConfusionHom_All3_obligation_2 A B C R [] [] [] All3_nil All3_nil
         eq_refl) = eq_refl)

  
  A : Type
  B : Type
  C : Type
  R : A → B → C → Type
  x : A
  y : B
  z : C
  l : list A
  l' : list B
  l'' : list C
  r : R x y z
  a : All3 R l l' l''
  ============================
   (noConfusionHom_All3_obligation_1 A B C R (x :: l) 
      (y :: l') (z :: l'') (All3_cons r a) (All3_cons r a)
      (noConfusionHom_All3_obligation_2 A B C R (x :: l) 
         (y :: l') (z :: l'') (All3_cons r a) (All3_cons r a) eq_refl) =
    eq_refl)


DEBUG:Going to execute:
CoreTactics.unblock_goal

Goals:
    A : Type  B : Type  C : Type  R : A → B → C → Type
  ============================
   (noConfusionHom_All3_obligation_1 A B C R [] [] [] All3_nil All3_nil
      (noConfusionHom_All3_obligation_2 A B C R [] [] [] All3_nil All3_nil
         eq_refl) = eq_refl)

  
  A : Type
  B : Type
  C : Type
  R : A → B → C → Type
  x : A
  y : B
  z : C
  l : list A
  l' : list B
  l'' : list C
  r : R x y z
  a : All3 R l l' l''
  ============================
   (noConfusionHom_All3_obligation_1 A B C R (x :: l) 
      (y :: l') (z :: l'') (All3_cons r a) (All3_cons r a)
      (noConfusionHom_All3_obligation_2 A B C R (x :: l) 
         (y :: l') (z :: l'') (All3_cons r a) (All3_cons r a) eq_refl) =
    eq_refl)


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

Goals:
    A : Type  B : Type  C : Type  R : A → B → C → Type
  ============================
   (noConfusionHom_All3_obligation_1 A B C R [] [] [] All3_nil All3_nil
      (noConfusionHom_All3_obligation_2 A B C R [] [] [] All3_nil All3_nil
         eq_refl) = eq_refl)

  
  A : Type
  B : Type
  C : Type
  R : A → B → C → Type
  x : A
  y : B
  z : C
  l : list A
  l' : list B
  l'' : list C
  r : R x y z
  a : All3 R l l' l''
  ============================
   (noConfusionHom_All3_obligation_1 A B C R (x :: l) 
      (y :: l') (z :: l'') (All3_cons r a) (All3_cons r a)
      (noConfusionHom_All3_obligation_2 A B C R (x :: l) 
         (y :: l') (z :: l'') (All3_cons r a) (All3_cons r a) eq_refl) =
    eq_refl)


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

Goals:
    A : Type  B : Type  C : Type  R : A → B → C → Type
  ============================
   (noConfusionHom_All3_obligation_1 A B C R [] [] [] All3_nil All3_nil
      (noConfusionHom_All3_obligation_2 A B C R [] [] [] All3_nil All3_nil
         eq_refl) = eq_refl)

  
  A : Type
  B : Type
  C : Type
  R : A → B → C → Type
  x : A
  y : B
  z : C
  l : list A
  l' : list B
  l'' : list C
  r : R x y z
  a : All3 R l l' l''
  ============================
   (noConfusionHom_All3_obligation_1 A B C R (x :: l) 
      (y :: l') (z :: l'') (All3_cons r a) (All3_cons r a)
      (noConfusionHom_All3_obligation_2 A B C R (x :: l) 
         (y :: l') (z :: l'') (All3_cons r a) (All3_cons r a) eq_refl) =
    eq_refl)


DEBUG:Going to execute:
cbv zeta

Goals:
    A : Type  B : Type  C : Type  R : A → B → C → Type
  ============================
   (noConfusionHom_All3_obligation_1 A B C R [] [] [] All3_nil All3_nil
      (noConfusionHom_All3_obligation_2 A B C R [] [] [] All3_nil All3_nil
         eq_refl) = eq_refl)

  
  A : Type
  B : Type
  C : Type
  R : A → B → C → Type
  x : A
  y : B
  z : C
  l : list A
  l' : list B
  l'' : list C
  r : R x y z
  a : All3 R l l' l''
  ============================
   (noConfusionHom_All3_obligation_1 A B C R (x :: l) 
      (y :: l') (z :: l'') (All3_cons r a) (All3_cons r a)
      (noConfusionHom_All3_obligation_2 A B C R (x :: l) 
         (y :: l') (z :: l'') (All3_cons r a) (All3_cons r a) 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  C : Type  R : A → B → C → Type
  ============================
   (apply_noConfusion [] []
      (Logic.True_rect_dep
         (λ H : True,
            ∀ e : {| pr1 := []; pr2 := [] |} = {| pr1 := []; pr2 := [] |},
              eq_rect {| pr1 := []; pr2 := {| pr1 := []; pr2 := [] |} |}
                (λ index : sigma (λ _ : list A, sigma (λ _ : list B, list C)),
                   All3 R (pr1 index) (pr1 (pr2 index)) (pr2 (pr2 index)))
                All3_nil {| pr1 := []; pr2 := {| pr1 := []; pr2 := [] |} |}
                (DepElim.pack_sigma_eq_nondep match H with
                                              | I => eq_refl
                                              end e) = All3_nil
              → apply_noConfusion [] []
                  (λ _ : True,
                     DepElim.eq_simplification_sigma1 [] [] [] []
                       (apply_noConfusion [] []
                          (λ _ : True,
                             apply_noConfusion [] [] (λ _ : True, True))))
                  eq_refl eq_refl → All3_nil = All3_nil)
         (DepElim.eq_simplification_sigma1_nondep_dep [] [] [] []
            (apply_noConfusion [] []
               (Logic.True_rect_dep
                  (λ H : True,
                     ∀ e : [] = [],
                       eq_rect
                         {| pr1 := []; pr2 := {| pr1 := []; pr2 := [] |} |}
                         (λ index : sigma
                                      (λ _ : list A,
                                         sigma (λ _ : list B, list C)),
                            All3 R (pr1 index) (pr1 (pr2 index))
                              (pr2 (pr2 index))) All3_nil
                         {| pr1 := []; pr2 := {| pr1 := []; pr2 := [] |} |}
                         match
                           DepElim.pack_sigma_eq_nondep
                             match H with
                             | I => eq_refl
                             end e in (_ = p)
                           return
                             ({|
                                pr1 := []; pr2 := {| pr1 := []; pr2 := [] |}
                              |} = {| pr1 := []; pr2 := p |})
                         with
                         | eq_refl => eq_refl
                         end = All3_nil
                       → apply_noConfusion [] []
                           (λ _ : True,
                              DepElim.eq_simplification_sigma1 [] [] [] []
                                (apply_noConfusion [] []
                                   (λ _ : True,
                                      apply_noConfusion [] []
                                        (λ _ : True, True)))) eq_refl eq_refl
                         → All3_nil = All3_nil)
                  (apply_noConfusion [] []
                     (Logic.True_rect_dep
                        (λ H : True,
                           eq_rect
                             {|
                               pr1 := []; pr2 := {| pr1 := []; pr2 := [] |}
                             |}
                             (λ index : sigma
                                          (λ _ : list A,
                                             sigma (λ _ : list B, list C)),
                                All3 R (pr1 index) 
                                  (pr1 (pr2 index)) 
                                  (pr2 (pr2 index))) All3_nil
                             {|
                               pr1 := []; pr2 := {| pr1 := []; pr2 := [] |}
                             |}
                             match
                               match
                                 match H with
                                 | I => eq_refl
                                 end in (_ = p)
                                 return
                                   ({| pr1 := []; pr2 := [] |} =
                                    {| pr1 := []; pr2 := p |})
                               with
                               | eq_refl => eq_refl
                               end in (_ = p)
                               return
                                 ({|
                                    pr1 := [];
                                    pr2 := {| pr1 := []; pr2 := [] |}
                                  |} = {| pr1 := []; pr2 := p |})
                             with
                             | eq_refl => eq_refl
                             end = All3_nil
                           → apply_noConfusion [] []
                               (λ _ : True,
                                  DepElim.eq_simplification_sigma1 [] [] []
                                    []
                                    (apply_noConfusion [] []
                                       (λ _ : True,
                                          apply_noConfusion [] []
                                            (λ _ : True, True)))) eq_refl
                               eq_refl → All3_nil = All3_nil)
                        (λ H : All3_nil = All3_nil,
                           DepElim.solution_left All3_nil
                             (λ H0 : apply_noConfusion [] []
                                       (λ _ : True,
                                          DepElim.eq_simplification_sigma1 []
                                            [] [] []
                                            (apply_noConfusion [] []
                                               (λ _ : True,
                                                 apply_noConfusion [] []
                                                 (λ _ : True, True))))
                                       eq_refl eq_refl,
                                match H0 with
                                | I => eq_refl
                                end) All3_nil H))))))) eq_refl eq_refl
      eq_refl I = eq_refl)

  
  A : Type
  B : Type
  C : Type
  R : A → B → C → Type
  x : A
  y : B
  z : C
  l : list A
  l' : list B
  l'' : list C
  r : R x y z
  a : All3 R l l' l''
  ============================
   (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) (z0 : C) (l0 : list A) (l'0 : list B) 
                 (l''0 : list C) (r0 : R x y0 z0) 
                 (b : All3 R l0 l'0 l''0) (e : l = l0),
                 DepElim.solution_right_dep l
                   (λ (l'1 : list B) (l''1 : list C) 
                      (r1 : R x y0 z0) (b0 : All3 R l l'1 l''1),
                      DepElim.eq_simplification_sigma1_nondep_dep 
                        (y :: l') (y0 :: l'1) (z :: l'') 
                        (z0 :: l''1)
                        (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
                                   (λ (z1 : C) (l'2 : list B) 
                                      (l''2 : list C) 
                                      (r2 : R x y z1) 
                                      (b1 : All3 R l l'2 l''2) 
                                      (e0 : l' = l'2),
                                      DepElim.solution_right_dep l'
                                        (λ (l''3 : list C) 
                                           (r3 : R x y z1) 
                                           (b2 : All3 R l l' l''3),
                                           apply_noConfusion 
                                             (z :: l'') 
                                             (z1 :: l''3)
                                             (DepElim.eq_simplification_sigma1_nondep_dep
                                                z z1 l'' l''3
                                                (λ e'1 : z = z1,
                                                 DepElim.solution_right_dep z
                                                 (λ (l''4 : list C) 
                                                 (r4 : 
                                                 R x y z) 
                                                 (b3 : 
                                                 All3 R l l' l''4) 
                                                 (e1 : 
                                                 l'' = l''4),
                                                 DepElim.solution_right_dep
                                                 l''
                                                 (λ (r5 : R x y z) 
                                                 (b4 : 
                                                 All3 R l l' l'') 
                                                 (H : 
                                                 All3_cons r a =
                                                 All3_cons r5 b4),
                                                 DepElim.solution_left
                                                 (All3_cons r5 b4)
                                                 (λ H0 : 
                                                 apply_noConfusion 
                                                 (x :: l) 
                                                 (x :: l)
                                                 (DepElim.eq_simplification_sigma1
                                                 x x l l
                                                 (λ H0 : x = x,
                                                 DepElim.solution_left x
                                                 (λ (y1 : B) 
                                                 (z2 : C) 
                                                 (l1 : list A) 
                                                 (l'3 : list B) 
                                                 (l''5 : 
                                                 list C) 
                                                 (y2 : R x y1 z2) 
                                                 (a0 : 
                                                 All3 R l1 l'3 l''5) 
                                                 (H1 : 
                                                 l1 = l),
                                                 DepElim.solution_left l
                                                 (λ (l'4 : list B) 
                                                 (l''6 : 
                                                 list C) 
                                                 (y3 : R x y1 z2) 
                                                 (a1 : 
                                                 All3 R l l'4 l''6),
                                                 DepElim.eq_simplification_sigma1
                                                 (y1 :: l'4) 
                                                 (y :: l') 
                                                 (z2 :: l''6) 
                                                 (z :: l'')
                                                 (apply_noConfusion
                                                 (y1 :: l'4) 
                                                 (y :: l')
                                                 (DepElim.eq_simplification_sigma1
                                                 y1 y l'4 l'
                                                 (λ H2 : y1 = y,
                                                 DepElim.solution_left y
                                                 (λ (z3 : C) 
                                                 (l'5 : list B) 
                                                 (l''7 : 
                                                 list C) 
                                                 (y4 : R x y z3) 
                                                 (a2 : 
                                                 All3 R l l'5 l''7) 
                                                 (H3 : 
                                                 l'5 = l'),
                                                 DepElim.solution_left l'
                                                 (λ (l''8 : list C) 
                                                 (y5 : 
                                                 R x y z3) 
                                                 (a3 : 
                                                 All3 R l l' l''8),
                                                 apply_noConfusion
                                                 (z3 :: l''8) 
                                                 (z :: l'')
                                                 (DepElim.eq_simplification_sigma1
                                                 z3 z l''8 l''
                                                 (λ H4 : z3 = z,
                                                 DepElim.solution_left z
                                                 (λ (l''9 : list C) 
                                                 (y6 : 
                                                 R x y z) 
                                                 (a4 : 
                                                 All3 R l l' l''9) 
                                                 (H5 : 
                                                 l''9 = l''),
                                                 DepElim.solution_left l''
                                                 (λ (y7 : R x y z) 
                                                 (a5 : 
                                                 All3 R l l' l''),
                                                 {| pr1 := r; pr2 := a |} =
                                                 {| pr1 := y7; pr2 := a5 |})
                                                 l''9 H5 y6 a4) z3 H4 l''8 y5
                                                 a3))) l'5 H3 l''7 y4 a2) y1
                                                 H2 z2 l'4 l''6 y3 a1)))) l1
                                                 H1 l'3 l''5 y2 a0) x H0 y z
                                                 l l' l'' r5 b4)) eq_refl
                                                 eq_refl,
                                                 match
                                                 H0 in (_ = s)
                                                 return
                                                 (All3_cons r a =
                                                 All3_cons (pr1 s) (pr2 s))
                                                 with
                                                 | eq_refl => eq_refl
                                                 end) 
                                                 (All3_cons r a) H) l''4 e1
                                                 r4 b3) z1 e'1 l''3 r3 b2)))
                                        l'2 e0 l''2 r2 b1) y0 e'0 z0 l'1 l''1
                                   r1 b0)))) l0 e l'0 l''0 r0 b) x e' y z l
              l' l'' r a)) eq_refl eq_refl eq_refl eq_refl = eq_refl)


DEBUG:Going to execute:
DepElim.simpl_equations

Goals:
    A : Type  B : Type  C : Type  R : A → B → C → Type
  ============================
   (apply_noConfusion [] []
      (Logic.True_rect_dep
         (λ H : True,
            ∀ e : {| pr1 := []; pr2 := [] |} = {| pr1 := []; pr2 := [] |},
              eq_rect {| pr1 := []; pr2 := {| pr1 := []; pr2 := [] |} |}
                (λ index : sigma (λ _ : list A, sigma (λ _ : list B, list C)),
                   All3 R (pr1 index) (pr1 (pr2 index)) (pr2 (pr2 index)))
                All3_nil {| pr1 := []; pr2 := {| pr1 := []; pr2 := [] |} |}
                (DepElim.pack_sigma_eq_nondep match H with
                                              | I => eq_refl
                                              end e) = All3_nil
              → apply_noConfusion [] []
                  (λ _ : True,
                     DepElim.eq_simplification_sigma1 [] [] [] []
                       (apply_noConfusion [] []
                          (λ _ : True,
                             apply_noConfusion [] [] (λ _ : True, True))))
                  eq_refl eq_refl → All3_nil = All3_nil)
         (DepElim.eq_simplification_sigma1_nondep_dep [] [] [] []
            (apply_noConfusion [] []
               (Logic.True_rect_dep
                  (λ H : True,
                     ∀ e : [] = [],
                       eq_rect
                         {| pr1 := []; pr2 := {| pr1 := []; pr2 := [] |} |}
                         (λ index : sigma
                                      (λ _ : list A,
                                         sigma (λ _ : list B, list C)),
                            All3 R (pr1 index) (pr1 (pr2 index))
                              (pr2 (pr2 index))) All3_nil
                         {| pr1 := []; pr2 := {| pr1 := []; pr2 := [] |} |}
                         match
                           DepElim.pack_sigma_eq_nondep
                             match H with
                             | I => eq_refl
                             end e in (_ = p)
                           return
                             ({|
                                pr1 := []; pr2 := {| pr1 := []; pr2 := [] |}
                              |} = {| pr1 := []; pr2 := p |})
                         with
                         | eq_refl => eq_refl
                         end = All3_nil
                       → apply_noConfusion [] []
                           (λ _ : True,
                              DepElim.eq_simplification_sigma1 [] [] [] []
                                (apply_noConfusion [] []
                                   (λ _ : True,
                                      apply_noConfusion [] []
                                        (λ _ : True, True)))) eq_refl eq_refl
                         → All3_nil = All3_nil)
                  (apply_noConfusion [] []
                     (Logic.True_rect_dep
                        (λ H : True,
                           eq_rect
                             {|
                               pr1 := []; pr2 := {| pr1 := []; pr2 := [] |}
                             |}
                             (λ index : sigma
                                          (λ _ : list A,
                                             sigma (λ _ : list B, list C)),
                                All3 R (pr1 index) 
                                  (pr1 (pr2 index)) 
                                  (pr2 (pr2 index))) All3_nil
                             {|
                               pr1 := []; pr2 := {| pr1 := []; pr2 := [] |}
                             |}
                             match
                               match
                                 match H with
                                 | I => eq_refl
                                 end in (_ = p)
                                 return
                                   ({| pr1 := []; pr2 := [] |} =
                                    {| pr1 := []; pr2 := p |})
                               with
                               | eq_refl => eq_refl
                               end in (_ = p)
                               return
                                 ({|
                                    pr1 := [];
                                    pr2 := {| pr1 := []; pr2 := [] |}
                                  |} = {| pr1 := []; pr2 := p |})
                             with
                             | eq_refl => eq_refl
                             end = All3_nil
                           → apply_noConfusion [] []
                               (λ _ : True,
                                  DepElim.eq_simplification_sigma1 [] [] []
                                    []
                                    (apply_noConfusion [] []
                                       (λ _ : True,
                                          apply_noConfusion [] []
                                            (λ _ : True, True)))) eq_refl
                               eq_refl → All3_nil = All3_nil)
                        (λ H : All3_nil = All3_nil,
                           DepElim.solution_left All3_nil
                             (λ H0 : apply_noConfusion [] []
                                       (λ _ : True,
                                          DepElim.eq_simplification_sigma1 []
                                            [] [] []
                                            (apply_noConfusion [] []
                                               (λ _ : True,
                                                 apply_noConfusion [] []
                                                 (λ _ : True, True))))
                                       eq_refl eq_refl,
                                match H0 with
                                | I => eq_refl
                                end) All3_nil H))))))) eq_refl eq_refl
      eq_refl I = eq_refl)

  
  A : Type
  B : Type
  C : Type
  R : A → B → C → Type
  x : A
  y : B
  z : C
  l : list A
  l' : list B
  l'' : list C
  r : R x y z
  a : All3 R l l' l''
  ============================
   (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) (z0 : C) (l0 : list A) (l'0 : list B) 
                 (l''0 : list C) (r0 : R x y0 z0) 
                 (b : All3 R l0 l'0 l''0) (e : l = l0),
                 DepElim.solution_right_dep l
                   (λ (l'1 : list B) (l''1 : list C) 
                      (r1 : R x y0 z0) (b0 : All3 R l l'1 l''1),
                      DepElim.eq_simplification_sigma1_nondep_dep 
                        (y :: l') (y0 :: l'1) (z :: l'') 
                        (z0 :: l''1)
                        (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
                                   (λ (z1 : C) (l'2 : list B) 
                                      (l''2 : list C) 
                                      (r2 : R x y z1) 
                                      (b1 : All3 R l l'2 l''2) 
                                      (e0 : l' = l'2),
                                      DepElim.solution_right_dep l'
                                        (λ (l''3 : list C) 
                                           (r3 : R x y z1) 
                                           (b2 : All3 R l l' l''3),
                                           apply_noConfusion 
                                             (z :: l'') 
                                             (z1 :: l''3)
                                             (DepElim.eq_simplification_sigma1_nondep_dep
                                                z z1 l'' l''3
                                                (λ e'1 : z = z1,
                                                 DepElim.solution_right_dep z
                                                 (λ (l''4 : list C) 
                                                 (r4 : 
                                                 R x y z) 
                                                 (b3 : 
                                                 All3 R l l' l''4) 
                                                 (e1 : 
                                                 l'' = l''4),
                                                 DepElim.solution_right_dep
                                                 l''
                                                 (λ (r5 : R x y z) 
                                                 (b4 : 
                                                 All3 R l l' l'') 
                                                 (H : 
                                                 All3_cons r a =
                                                 All3_cons r5 b4),
                                                 DepElim.solution_left
                                                 (All3_cons r5 b4)
                                                 (λ H0 : 
                                                 apply_noConfusion 
                                                 (x :: l) 
                                                 (x :: l)
                                                 (DepElim.eq_simplification_sigma1
                                                 x x l l
                                                 (λ H0 : x = x,
                                                 DepElim.solution_left x
                                                 (λ (y1 : B) 
                                                 (z2 : C) 
                                                 (l1 : list A) 
                                                 (l'3 : list B) 
                                                 (l''5 : 
                                                 list C) 
                                                 (y2 : R x y1 z2) 
                                                 (a0 : 
                                                 All3 R l1 l'3 l''5) 
                                                 (H1 : 
                                                 l1 = l),
                                                 DepElim.solution_left l
                                                 (λ (l'4 : list B) 
                                                 (l''6 : 
                                                 list C) 
                                                 (y3 : R x y1 z2) 
                                                 (a1 : 
                                                 All3 R l l'4 l''6),
                                                 DepElim.eq_simplification_sigma1
                                                 (y1 :: l'4) 
                                                 (y :: l') 
                                                 (z2 :: l''6) 
                                                 (z :: l'')
                                                 (apply_noConfusion
                                                 (y1 :: l'4) 
                                                 (y :: l')
                                                 (DepElim.eq_simplification_sigma1
                                                 y1 y l'4 l'
                                                 (λ H2 : y1 = y,
                                                 DepElim.solution_left y
                                                 (λ (z3 : C) 
                                                 (l'5 : list B) 
                                                 (l''7 : 
                                                 list C) 
                                                 (y4 : R x y z3) 
                                                 (a2 : 
                                                 All3 R l l'5 l''7) 
                                                 (H3 : 
                                                 l'5 = l'),
                                                 DepElim.solution_left l'
                                                 (λ (l''8 : list C) 
                                                 (y5 : 
                                                 R x y z3) 
                                                 (a3 : 
                                                 All3 R l l' l''8),
                                                 apply_noConfusion
                                                 (z3 :: l''8) 
                                                 (z :: l'')
                                                 (DepElim.eq_simplification_sigma1
                                                 z3 z l''8 l''
                                                 (λ H4 : z3 = z,
                                                 DepElim.solution_left z
                                                 (λ (l''9 : list C) 
                                                 (y6 : 
                                                 R x y z) 
                                                 (a4 : 
                                                 All3 R l l' l''9) 
                                                 (H5 : 
                                                 l''9 = l''),
                                                 DepElim.solution_left l''
                                                 (λ (y7 : R x y z) 
                                                 (a5 : 
                                                 All3 R l l' l''),
                                                 {| pr1 := r; pr2 := a |} =
                                                 {| pr1 := y7; pr2 := a5 |})
                                                 l''9 H5 y6 a4) z3 H4 l''8 y5
                                                 a3))) l'5 H3 l''7 y4 a2) y1
                                                 H2 z2 l'4 l''6 y3 a1)))) l1
                                                 H1 l'3 l''5 y2 a0) x H0 y z
                                                 l l' l'' r5 b4)) eq_refl
                                                 eq_refl,
                                                 match
                                                 H0 in (_ = s)
                                                 return
                                                 (All3_cons r a =
                                                 All3_cons (pr1 s) (pr2 s))
                                                 with
                                                 | eq_refl => eq_refl
                                                 end) 
                                                 (All3_cons r a) H) l''4 e1
                                                 r4 b3) z1 e'1 l''3 r3 b2)))
                                        l'2 e0 l''2 r2 b1) y0 e'0 z0 l'1 l''1
                                   r1 b0)))) l0 e l'0 l''0 r0 b) x e' y z l
              l' l'' r a)) 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)