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''
  r0 : R x y z
  b : All3 R l l' l''
  e : NoConfusionHom_All3 A B C R (x :: l) (y :: l') 
        (z :: l'') (All3_cons r a) (All3_cons r0 b)
  ============================
   (let H := CoreTactics.block in
    noConfusionHom_All3_obligation_2 A B C R (x :: l) 
      (y :: l') (z :: l'') (All3_cons r a) (All3_cons r0 b)
      (noConfusionHom_All3_obligation_1 A B C R (x :: l) 
         (y :: l') (z :: l'') (All3_cons r a) (All3_cons r0 b) e) = e)


DEBUG:Going to execute:
intros _

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

  
  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''
  r0 : R x y z
  b : All3 R l l' l''
  e : NoConfusionHom_All3 A B C R (x :: l) (y :: l') 
        (z :: l'') (All3_cons r a) (All3_cons r0 b)
  ============================
   (noConfusionHom_All3_obligation_2 A B C R (x :: l) 
      (y :: l') (z :: l'') (All3_cons r a) (All3_cons r0 b)
      (noConfusionHom_All3_obligation_1 A B C R (x :: l) 
         (y :: l') (z :: l'') (All3_cons r a) (All3_cons r0 b) e) = e)


DEBUG:Going to execute:
CoreTactics.unblock_goal

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

  
  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''
  r0 : R x y z
  b : All3 R l l' l''
  e : NoConfusionHom_All3 A B C R (x :: l) (y :: l') 
        (z :: l'') (All3_cons r a) (All3_cons r0 b)
  ============================
   (noConfusionHom_All3_obligation_2 A B C R (x :: l) 
      (y :: l') (z :: l'') (All3_cons r a) (All3_cons r0 b)
      (noConfusionHom_All3_obligation_1 A B C R (x :: l) 
         (y :: l') (z :: l'') (All3_cons r a) (All3_cons r0 b) e) = e)


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

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

  
  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''
  r0 : R x y z
  b : All3 R l l' l''
  e : NoConfusionHom_All3 A B C R (x :: l) (y :: l') 
        (z :: l'') (All3_cons r a) (All3_cons r0 b)
  ============================
   (noConfusionHom_All3_obligation_2 A B C R (x :: l) 
      (y :: l') (z :: l'') (All3_cons r a) (All3_cons r0 b)
      (noConfusionHom_All3_obligation_1 A B C R (x :: l) 
         (y :: l') (z :: l'') (All3_cons r a) (All3_cons r0 b) e) = e)


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

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

  
  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''
  r0 : R x y z
  b : All3 R l l' l''
  e : NoConfusionHom_All3 A B C R (x :: l) (y :: l') 
        (z :: l'') (All3_cons r a) (All3_cons r0 b)
  ============================
   (noConfusionHom_All3_obligation_2 A B C R (x :: l) 
      (y :: l') (z :: l'') (All3_cons r a) (All3_cons r0 b)
      (noConfusionHom_All3_obligation_1 A B C R (x :: l) 
         (y :: l') (z :: l'') (All3_cons r a) (All3_cons r0 b) e) = e)


DEBUG:Going to execute:
cbv zeta

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

  
  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''
  r0 : R x y z
  b : All3 R l l' l''
  e : NoConfusionHom_All3 A B C R (x :: l) (y :: l') 
        (z :: l'') (All3_cons r a) (All3_cons r0 b)
  ============================
   (noConfusionHom_All3_obligation_2 A B C R (x :: l) 
      (y :: l') (z :: l'') (All3_cons r a) (All3_cons r0 b)
      (noConfusionHom_All3_obligation_1 A B C R (x :: l) 
         (y :: l') (z :: l'') (All3_cons r a) (All3_cons r0 b) e) = e)


DEBUG:Going to execute:
simpl in * |-

Goals:
  
  A : Type
  B : Type
  C : Type
  R : A → B → C → Type
  e : apply_noConfusion [] []
        (λ _ : True,
           DepElim.eq_simplification_sigma1 [] [] [] []
             (apply_noConfusion [] []
                (λ _ : True, apply_noConfusion [] [] (λ _ : True, True))))
        eq_refl eq_refl
  ============================
   (noConfusionHom_All3_obligation_2 A B C R [] [] [] All3_nil All3_nil
      (noConfusionHom_All3_obligation_1 A B C R [] [] [] All3_nil All3_nil e) =
    e)

  
  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''
  r0 : R x y z
  b : All3 R l l' l''
  e : apply_noConfusion (x :: l) (x :: l)
        (DepElim.eq_simplification_sigma1 x x l l
           (λ H : x = x,
              DepElim.solution_left x
                (λ (y0 : B) (z0 : C) (l0 : list A) 
                   (l'0 : list B) (l''0 : list C) 
                   (y1 : R x y0 z0) (a0 : All3 R l0 l'0 l''0) 
                   (H0 : l0 = l),
                   DepElim.solution_left l
                     (λ (l'1 : list B) (l''1 : list C) 
                        (y2 : R x y0 z0) (a1 : All3 R l l'1 l''1),
                        DepElim.eq_simplification_sigma1 
                          (y0 :: l'1) (y :: l') (z0 :: l''1) 
                          (z :: l'')
                          (apply_noConfusion (y0 :: l'1) 
                             (y :: l')
                             (DepElim.eq_simplification_sigma1 y0 y l'1 l'
                                (λ H1 : y0 = y,
                                   DepElim.solution_left y
                                     (λ (z1 : C) (l'2 : list B) 
                                        (l''2 : list C) 
                                        (y3 : R x y z1) 
                                        (a2 : All3 R l l'2 l''2) 
                                        (H2 : l'2 = l'),
                                        DepElim.solution_left l'
                                          (λ (l''3 : list C) 
                                             (y4 : R x y z1) 
                                             (a3 : 
                                              All3 R l l' l''3),
                                             apply_noConfusion 
                                               (z1 :: l''3) 
                                               (z :: l'')
                                               (DepElim.eq_simplification_sigma1
                                                 z1 z l''3 l''
                                                 (λ H3 : z1 = z,
                                                 DepElim.solution_left z
                                                 (λ (l''4 : list C) 
                                                 (y5 : 
                                                 R x y z) 
                                                 (a4 : 
                                                 All3 R l l' l''4) 
                                                 (H4 : 
                                                 l''4 = l''),
                                                 DepElim.solution_left l''
                                                 (λ (y6 : R x y z) 
                                                 (a5 : 
                                                 All3 R l l' l''),
                                                 {| pr1 := r; pr2 := a |} =
                                                 {| pr1 := y6; pr2 := a5 |})
                                                 l''4 H4 y5 a4) z1 H3 l''3 y4
                                                 a3))) l'2 H2 l''2 y3 a2) y0
                                     H1 z0 l'1 l''1 y2 a1)))) l0 H0 l'0 l''0
                     y1 a0) x H y z l l' l'' r0 b)) eq_refl eq_refl
  ============================
   (noConfusionHom_All3_obligation_2 A B C R (x :: l) 
      (y :: l') (z :: l'') (All3_cons r a) (All3_cons r0 b)
      (noConfusionHom_All3_obligation_1 A B C R (x :: l) 
         (y :: l') (z :: l'') (All3_cons r a) (All3_cons r0 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
  C : Type
  R : A → B → C → Type
  e : apply_noConfusion [] []
        (λ _ : True,
           DepElim.eq_simplification_sigma1 [] [] [] []
             (apply_noConfusion [] []
                (λ _ : True, apply_noConfusion [] [] (λ _ : True, True))))
        eq_refl eq_refl
  ============================
   (noConfusionHom_All3_obligation_2 A B C R [] [] [] All3_nil All3_nil
      (noConfusionHom_All3_obligation_1 A B C R [] [] [] All3_nil All3_nil e) =
    e)

  
  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''
  r0 : R x y z
  b : All3 R l l' l''
  e : apply_noConfusion (x :: l) (x :: l)
        (DepElim.eq_simplification_sigma1 x x l l
           (λ H : x = x,
              DepElim.solution_left x
                (λ (y0 : B) (z0 : C) (l0 : list A) 
                   (l'0 : list B) (l''0 : list C) 
                   (y1 : R x y0 z0) (a0 : All3 R l0 l'0 l''0) 
                   (H0 : l0 = l),
                   DepElim.solution_left l
                     (λ (l'1 : list B) (l''1 : list C) 
                        (y2 : R x y0 z0) (a1 : All3 R l l'1 l''1),
                        DepElim.eq_simplification_sigma1 
                          (y0 :: l'1) (y :: l') (z0 :: l''1) 
                          (z :: l'')
                          (apply_noConfusion (y0 :: l'1) 
                             (y :: l')
                             (DepElim.eq_simplification_sigma1 y0 y l'1 l'
                                (λ H1 : y0 = y,
                                   DepElim.solution_left y
                                     (λ (z1 : C) (l'2 : list B) 
                                        (l''2 : list C) 
                                        (y3 : R x y z1) 
                                        (a2 : All3 R l l'2 l''2) 
                                        (H2 : l'2 = l'),
                                        DepElim.solution_left l'
                                          (λ (l''3 : list C) 
                                             (y4 : R x y z1) 
                                             (a3 : 
                                              All3 R l l' l''3),
                                             apply_noConfusion 
                                               (z1 :: l''3) 
                                               (z :: l'')
                                               (DepElim.eq_simplification_sigma1
                                                 z1 z l''3 l''
                                                 (λ H3 : z1 = z,
                                                 DepElim.solution_left z
                                                 (λ (l''4 : list C) 
                                                 (y5 : 
                                                 R x y z) 
                                                 (a4 : 
                                                 All3 R l l' l''4) 
                                                 (H4 : 
                                                 l''4 = l''),
                                                 DepElim.solution_left l''
                                                 (λ (y6 : R x y z) 
                                                 (a5 : 
                                                 All3 R l l' l''),
                                                 {| pr1 := r; pr2 := a |} =
                                                 {| pr1 := y6; pr2 := a5 |})
                                                 l''4 H4 y5 a4) z1 H3 l''3 y4
                                                 a3))) l'2 H2 l''2 y3 a2) y0
                                     H1 z0 l'1 l''1 y2 a1)))) l0 H0 l'0 l''0
                     y1 a0) x H y z l l' l'' r0 b)) eq_refl eq_refl
  ============================
   (noConfusionHom_All3_obligation_2 A B C R (x :: l) 
      (y :: l') (z :: l'') (All3_cons r a) (All3_cons r0 b)
      (noConfusionHom_All3_obligation_1 A B C R (x :: l) 
         (y :: l') (z :: l'') (All3_cons r a) (All3_cons r0 b) e) = e)


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

Goals:
  
  A : Type
  B : Type
  C : Type
  R : A → B → C → Type
  e : apply_noConfusion [] []
        (λ _ : True,
           DepElim.eq_simplification_sigma1 [] [] [] []
             (apply_noConfusion [] []
                (λ _ : True, apply_noConfusion [] [] (λ _ : True, True))))
        eq_refl eq_refl
  ============================
   (noConfusionHom_All3_obligation_2 A B C R [] [] [] All3_nil All3_nil
      (noConfusionHom_All3_obligation_1 A B C R [] [] [] All3_nil All3_nil e) =
    e)

  
  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''
  r0 : R x y z
  b : All3 R l l' l''
  e : apply_noConfusion (x :: l) (x :: l)
        (DepElim.eq_simplification_sigma1 x x l l
           (λ H : x = x,
              DepElim.solution_left x
                (λ (y0 : B) (z0 : C) (l0 : list A) 
                   (l'0 : list B) (l''0 : list C) 
                   (y1 : R x y0 z0) (a0 : All3 R l0 l'0 l''0) 
                   (H0 : l0 = l),
                   DepElim.solution_left l
                     (λ (l'1 : list B) (l''1 : list C) 
                        (y2 : R x y0 z0) (a1 : All3 R l l'1 l''1),
                        DepElim.eq_simplification_sigma1 
                          (y0 :: l'1) (y :: l') (z0 :: l''1) 
                          (z :: l'')
                          (apply_noConfusion (y0 :: l'1) 
                             (y :: l')
                             (DepElim.eq_simplification_sigma1 y0 y l'1 l'
                                (λ H1 : y0 = y,
                                   DepElim.solution_left y
                                     (λ (z1 : C) (l'2 : list B) 
                                        (l''2 : list C) 
                                        (y3 : R x y z1) 
                                        (a2 : All3 R l l'2 l''2) 
                                        (H2 : l'2 = l'),
                                        DepElim.solution_left l'
                                          (λ (l''3 : list C) 
                                             (y4 : R x y z1) 
                                             (a3 : 
                                              All3 R l l' l''3),
                                             apply_noConfusion 
                                               (z1 :: l''3) 
                                               (z :: l'')
                                               (DepElim.eq_simplification_sigma1
                                                 z1 z l''3 l''
                                                 (λ H3 : z1 = z,
                                                 DepElim.solution_left z
                                                 (λ (l''4 : list C) 
                                                 (y5 : 
                                                 R x y z) 
                                                 (a4 : 
                                                 All3 R l l' l''4) 
                                                 (H4 : 
                                                 l''4 = l''),
                                                 DepElim.solution_left l''
                                                 (λ (y6 : R x y z) 
                                                 (a5 : 
                                                 All3 R l l' l''),
                                                 {| pr1 := r; pr2 := a |} =
                                                 {| pr1 := y6; pr2 := a5 |})
                                                 l''4 H4 y5 a4) z1 H3 l''3 y4
                                                 a3))) l'2 H2 l''2 y3 a2) y0
                                     H1 z0 l'1 l''1 y2 a1)))) l0 H0 l'0 l''0
                     y1 a0) x H y z l l' l'' r0 b)) eq_refl eq_refl
  ============================
   (noConfusionHom_All3_obligation_2 A B C R (x :: l) 
      (y :: l') (z :: l'') (All3_cons r a) (All3_cons r0 b)
      (noConfusionHom_All3_obligation_1 A B C R (x :: l) 
         (y :: l') (z :: l'') (All3_cons r a) (All3_cons r0 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
  C : Type
  R : A → B → C → Type
  e : apply_noConfusion [] []
        (λ _ : True,
           DepElim.eq_simplification_sigma1 [] [] [] []
             (apply_noConfusion [] []
                (λ _ : True, apply_noConfusion [] [] (λ _ : True, True))))
        eq_refl eq_refl
  ============================
   (noConfusionHom_All3_obligation_2 A B C R [] [] [] All3_nil All3_nil
      (noConfusionHom_All3_obligation_1 A B C R [] [] [] All3_nil All3_nil e) =
    e)

  
  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''
  r0 : R x y z
  b : All3 R l l' l''
  e : apply_noConfusion (x :: l) (x :: l)
        (DepElim.eq_simplification_sigma1 x x l l
           (λ H : x = x,
              DepElim.solution_left x
                (λ (y0 : B) (z0 : C) (l0 : list A) 
                   (l'0 : list B) (l''0 : list C) 
                   (y1 : R x y0 z0) (a0 : All3 R l0 l'0 l''0) 
                   (H0 : l0 = l),
                   DepElim.solution_left l
                     (λ (l'1 : list B) (l''1 : list C) 
                        (y2 : R x y0 z0) (a1 : All3 R l l'1 l''1),
                        DepElim.eq_simplification_sigma1 
                          (y0 :: l'1) (y :: l') (z0 :: l''1) 
                          (z :: l'')
                          (apply_noConfusion (y0 :: l'1) 
                             (y :: l')
                             (DepElim.eq_simplification_sigma1 y0 y l'1 l'
                                (λ H1 : y0 = y,
                                   DepElim.solution_left y
                                     (λ (z1 : C) (l'2 : list B) 
                                        (l''2 : list C) 
                                        (y3 : R x y z1) 
                                        (a2 : All3 R l l'2 l''2) 
                                        (H2 : l'2 = l'),
                                        DepElim.solution_left l'
                                          (λ (l''3 : list C) 
                                             (y4 : R x y z1) 
                                             (a3 : 
                                              All3 R l l' l''3),
                                             apply_noConfusion 
                                               (z1 :: l''3) 
                                               (z :: l'')
                                               (DepElim.eq_simplification_sigma1
                                                 z1 z l''3 l''
                                                 (λ H3 : z1 = z,
                                                 DepElim.solution_left z
                                                 (λ (l''4 : list C) 
                                                 (y5 : 
                                                 R x y z) 
                                                 (a4 : 
                                                 All3 R l l' l''4) 
                                                 (H4 : 
                                                 l''4 = l''),
                                                 DepElim.solution_left l''
                                                 (λ (y6 : R x y z) 
                                                 (a5 : 
                                                 All3 R l l' l''),
                                                 {| pr1 := r; pr2 := a |} =
                                                 {| pr1 := y6; pr2 := a5 |})
                                                 l''4 H4 y5 a4) z1 H3 l''3 y4
                                                 a3))) l'2 H2 l''2 y3 a2) y0
                                     H1 z0 l'1 l''1 y2 a1)))) l0 H0 l'0 l''0
                     y1 a0) x H y z l l' l'' r0 b)) eq_refl eq_refl
  ============================
   (noConfusionHom_All3_obligation_2 A B C R (x :: l) 
      (y :: l') (z :: l'') (All3_cons r a) (All3_cons r0 b)
      (noConfusionHom_All3_obligation_1 A B C R (x :: l) 
         (y :: l') (z :: l'') (All3_cons r a) (All3_cons r0 b) e) = e)


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