Goal:
  
  A : Type
  B : Type
  R : nat → A → B → Type
  n : nat
  x : A
  y : B
  l : list A
  r : list B
  r0 : R n x y
  a : All2i R (S n) l r
  r2 : R n x y
  b : All2i R (S n) l r
  e : NoConfusionHom_All2i A B R n (x :: l) (y :: r) 
        (All2i_cons r0 a) (All2i_cons r2 b)
  ============================
   (let H := CoreTactics.block in
    noConfusionHom_All2i_obligation_2 A B R n (x :: l) 
      (y :: r) (All2i_cons r0 a) (All2i_cons r2 b)
      (noConfusionHom_All2i_obligation_1 A B R n (x :: l) 
         (y :: r) (All2i_cons r0 a) (All2i_cons r2 b) e) = e)


DEBUG:Going to execute:
intros _

Goals:
  
  A : Type
  B : Type
  R : nat → A → B → Type
  n : nat
  e : NoConfusionHom_All2i A B R n [] [] All2i_nil All2i_nil
  ============================
   (noConfusionHom_All2i_obligation_2 A B R n [] [] All2i_nil All2i_nil
      (noConfusionHom_All2i_obligation_1 A B R n [] [] All2i_nil All2i_nil e) =
    e)

  
  A : Type
  B : Type
  R : nat → A → B → Type
  n : nat
  x : A
  y : B
  l : list A
  r : list B
  r0 : R n x y
  a : All2i R (S n) l r
  r2 : R n x y
  b : All2i R (S n) l r
  e : NoConfusionHom_All2i A B R n (x :: l) (y :: r) 
        (All2i_cons r0 a) (All2i_cons r2 b)
  ============================
   (noConfusionHom_All2i_obligation_2 A B R n (x :: l) 
      (y :: r) (All2i_cons r0 a) (All2i_cons r2 b)
      (noConfusionHom_All2i_obligation_1 A B R n (x :: l) 
         (y :: r) (All2i_cons r0 a) (All2i_cons r2 b) e) = e)


DEBUG:Going to execute:
CoreTactics.unblock_goal

Goals:
  
  A : Type
  B : Type
  R : nat → A → B → Type
  n : nat
  e : NoConfusionHom_All2i A B R n [] [] All2i_nil All2i_nil
  ============================
   (noConfusionHom_All2i_obligation_2 A B R n [] [] All2i_nil All2i_nil
      (noConfusionHom_All2i_obligation_1 A B R n [] [] All2i_nil All2i_nil e) =
    e)

  
  A : Type
  B : Type
  R : nat → A → B → Type
  n : nat
  x : A
  y : B
  l : list A
  r : list B
  r0 : R n x y
  a : All2i R (S n) l r
  r2 : R n x y
  b : All2i R (S n) l r
  e : NoConfusionHom_All2i A B R n (x :: l) (y :: r) 
        (All2i_cons r0 a) (All2i_cons r2 b)
  ============================
   (noConfusionHom_All2i_obligation_2 A B R n (x :: l) 
      (y :: r) (All2i_cons r0 a) (All2i_cons r2 b)
      (noConfusionHom_All2i_obligation_1 A B R n (x :: l) 
         (y :: r) (All2i_cons r0 a) (All2i_cons r2 b) e) = e)


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

Goals:
  
  A : Type
  B : Type
  R : nat → A → B → Type
  n : nat
  e : NoConfusionHom_All2i A B R n [] [] All2i_nil All2i_nil
  ============================
   (noConfusionHom_All2i_obligation_2 A B R n [] [] All2i_nil All2i_nil
      (noConfusionHom_All2i_obligation_1 A B R n [] [] All2i_nil All2i_nil e) =
    e)

  
  A : Type
  B : Type
  R : nat → A → B → Type
  n : nat
  x : A
  y : B
  l : list A
  r : list B
  r0 : R n x y
  a : All2i R (S n) l r
  r2 : R n x y
  b : All2i R (S n) l r
  e : NoConfusionHom_All2i A B R n (x :: l) (y :: r) 
        (All2i_cons r0 a) (All2i_cons r2 b)
  ============================
   (noConfusionHom_All2i_obligation_2 A B R n (x :: l) 
      (y :: r) (All2i_cons r0 a) (All2i_cons r2 b)
      (noConfusionHom_All2i_obligation_1 A B R n (x :: l) 
         (y :: r) (All2i_cons r0 a) (All2i_cons r2 b) e) = e)


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

Goals:
  
  A : Type
  B : Type
  R : nat → A → B → Type
  n : nat
  e : NoConfusionHom_All2i A B R n [] [] All2i_nil All2i_nil
  ============================
   (noConfusionHom_All2i_obligation_2 A B R n [] [] All2i_nil All2i_nil
      (noConfusionHom_All2i_obligation_1 A B R n [] [] All2i_nil All2i_nil e) =
    e)

  
  A : Type
  B : Type
  R : nat → A → B → Type
  n : nat
  x : A
  y : B
  l : list A
  r : list B
  r0 : R n x y
  a : All2i R (S n) l r
  r2 : R n x y
  b : All2i R (S n) l r
  e : NoConfusionHom_All2i A B R n (x :: l) (y :: r) 
        (All2i_cons r0 a) (All2i_cons r2 b)
  ============================
   (noConfusionHom_All2i_obligation_2 A B R n (x :: l) 
      (y :: r) (All2i_cons r0 a) (All2i_cons r2 b)
      (noConfusionHom_All2i_obligation_1 A B R n (x :: l) 
         (y :: r) (All2i_cons r0 a) (All2i_cons r2 b) e) = e)


DEBUG:Going to execute:
cbv zeta

Goals:
  
  A : Type
  B : Type
  R : nat → A → B → Type
  n : nat
  e : NoConfusionHom_All2i A B R n [] [] All2i_nil All2i_nil
  ============================
   (noConfusionHom_All2i_obligation_2 A B R n [] [] All2i_nil All2i_nil
      (noConfusionHom_All2i_obligation_1 A B R n [] [] All2i_nil All2i_nil e) =
    e)

  
  A : Type
  B : Type
  R : nat → A → B → Type
  n : nat
  x : A
  y : B
  l : list A
  r : list B
  r0 : R n x y
  a : All2i R (S n) l r
  r2 : R n x y
  b : All2i R (S n) l r
  e : NoConfusionHom_All2i A B R n (x :: l) (y :: r) 
        (All2i_cons r0 a) (All2i_cons r2 b)
  ============================
   (noConfusionHom_All2i_obligation_2 A B R n (x :: l) 
      (y :: r) (All2i_cons r0 a) (All2i_cons r2 b)
      (noConfusionHom_All2i_obligation_1 A B R n (x :: l) 
         (y :: r) (All2i_cons r0 a) (All2i_cons r2 b) e) = e)


DEBUG:Going to execute:
simpl in * |-

Goals:
  
  A : Type
  B : Type
  R : nat → A → B → Type
  n : nat
  e : apply_noConfusion [] []
        (λ _ : True, apply_noConfusion [] [] (λ _ : True, True)) eq_refl
        eq_refl
  ============================
   (noConfusionHom_All2i_obligation_2 A B R n [] [] All2i_nil All2i_nil
      (noConfusionHom_All2i_obligation_1 A B R n [] [] All2i_nil All2i_nil e) =
    e)

  
  A : Type
  B : Type
  R : nat → A → B → Type
  n : nat
  x : A
  y : B
  l : list A
  r : list B
  r0 : R n x y
  a : All2i R (S n) l r
  r2 : R n x y
  b : All2i R (S n) l r
  e : apply_noConfusion (x :: l) (x :: l)
        (DepElim.eq_simplification_sigma1 x x l l
           (λ H : x = x,
              DepElim.solution_left x
                (λ (y0 : B) (l0 : list A) (r1 : list B) 
                   (y1 : R n x y0) (a0 : All2i R (S n) l0 r1) 
                   (H0 : l0 = l),
                   DepElim.solution_left l
                     (λ (r2 : list B) (y2 : R n x y0) 
                        (a1 : All2i R (S n) l r2),
                        apply_noConfusion (y0 :: r2) 
                          (y :: r)
                          (DepElim.eq_simplification_sigma1 y0 y r2 r
                             (λ H1 : y0 = y,
                                DepElim.solution_left y
                                  (λ (r3 : list B) 
                                     (y3 : R n x y) 
                                     (a2 : All2i R (S n) l r3) 
                                     (H2 : r3 = r),
                                     DepElim.solution_left r
                                       (λ (y4 : R n x y) 
                                          (a3 : All2i R (S n) l r),
                                          {| pr1 := r0; pr2 := a |} =
                                          {| pr1 := y4; pr2 := a3 |}) r3 H2
                                       y3 a2) y0 H1 r2 y2 a1))) l0 H0 r1 y1
                     a0) x H y l r r2 b)) eq_refl eq_refl
  ============================
   (noConfusionHom_All2i_obligation_2 A B R n (x :: l) 
      (y :: r) (All2i_cons r0 a) (All2i_cons r2 b)
      (noConfusionHom_All2i_obligation_1 A B R n (x :: l) 
         (y :: r) (All2i_cons r0 a) (All2i_cons r2 b) e) = e)


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

Goals:
  
  A : Type
  B : Type
  R : nat → A → B → Type
  n : nat
  e : apply_noConfusion [] []
        (λ _ : True, apply_noConfusion [] [] (λ _ : True, True)) eq_refl
        eq_refl
  ============================
   (noConfusionHom_All2i_obligation_2 A B R n [] [] All2i_nil All2i_nil
      (noConfusionHom_All2i_obligation_1 A B R n [] [] All2i_nil All2i_nil e) =
    e)

  
  A : Type
  B : Type
  R : nat → A → B → Type
  n : nat
  x : A
  y : B
  l : list A
  r : list B
  r0 : R n x y
  a : All2i R (S n) l r
  r2 : R n x y
  b : All2i R (S n) l r
  e : apply_noConfusion (x :: l) (x :: l)
        (DepElim.eq_simplification_sigma1 x x l l
           (λ H : x = x,
              DepElim.solution_left x
                (λ (y0 : B) (l0 : list A) (r1 : list B) 
                   (y1 : R n x y0) (a0 : All2i R (S n) l0 r1) 
                   (H0 : l0 = l),
                   DepElim.solution_left l
                     (λ (r2 : list B) (y2 : R n x y0) 
                        (a1 : All2i R (S n) l r2),
                        apply_noConfusion (y0 :: r2) 
                          (y :: r)
                          (DepElim.eq_simplification_sigma1 y0 y r2 r
                             (λ H1 : y0 = y,
                                DepElim.solution_left y
                                  (λ (r3 : list B) 
                                     (y3 : R n x y) 
                                     (a2 : All2i R (S n) l r3) 
                                     (H2 : r3 = r),
                                     DepElim.solution_left r
                                       (λ (y4 : R n x y) 
                                          (a3 : All2i R (S n) l r),
                                          {| pr1 := r0; pr2 := a |} =
                                          {| pr1 := y4; pr2 := a3 |}) r3 H2
                                       y3 a2) y0 H1 r2 y2 a1))) l0 H0 r1 y1
                     a0) x H y l r r2 b)) eq_refl eq_refl
  ============================
   (noConfusionHom_All2i_obligation_2 A B R n (x :: l) 
      (y :: r) (All2i_cons r0 a) (All2i_cons r2 b)
      (noConfusionHom_All2i_obligation_1 A B R n (x :: l) 
         (y :: r) (All2i_cons r0 a) (All2i_cons r2 b) e) = e)


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

Goals:
  
  A : Type
  B : Type
  R : nat → A → B → Type
  n : nat
  e : apply_noConfusion [] []
        (λ _ : True, apply_noConfusion [] [] (λ _ : True, True)) eq_refl
        eq_refl
  ============================
   (noConfusionHom_All2i_obligation_2 A B R n [] [] All2i_nil All2i_nil
      (noConfusionHom_All2i_obligation_1 A B R n [] [] All2i_nil All2i_nil e) =
    e)

  
  A : Type
  B : Type
  R : nat → A → B → Type
  n : nat
  x : A
  y : B
  l : list A
  r : list B
  r0 : R n x y
  a : All2i R (S n) l r
  r2 : R n x y
  b : All2i R (S n) l r
  e : apply_noConfusion (x :: l) (x :: l)
        (DepElim.eq_simplification_sigma1 x x l l
           (λ H : x = x,
              DepElim.solution_left x
                (λ (y0 : B) (l0 : list A) (r1 : list B) 
                   (y1 : R n x y0) (a0 : All2i R (S n) l0 r1) 
                   (H0 : l0 = l),
                   DepElim.solution_left l
                     (λ (r2 : list B) (y2 : R n x y0) 
                        (a1 : All2i R (S n) l r2),
                        apply_noConfusion (y0 :: r2) 
                          (y :: r)
                          (DepElim.eq_simplification_sigma1 y0 y r2 r
                             (λ H1 : y0 = y,
                                DepElim.solution_left y
                                  (λ (r3 : list B) 
                                     (y3 : R n x y) 
                                     (a2 : All2i R (S n) l r3) 
                                     (H2 : r3 = r),
                                     DepElim.solution_left r
                                       (λ (y4 : R n x y) 
                                          (a3 : All2i R (S n) l r),
                                          {| pr1 := r0; pr2 := a |} =
                                          {| pr1 := y4; pr2 := a3 |}) r3 H2
                                       y3 a2) y0 H1 r2 y2 a1))) l0 H0 r1 y1
                     a0) x H y l r r2 b)) eq_refl eq_refl
  ============================
   (noConfusionHom_All2i_obligation_2 A B R n (x :: l) 
      (y :: r) (All2i_cons r0 a) (All2i_cons r2 b)
      (noConfusionHom_All2i_obligation_1 A B R n (x :: l) 
         (y :: r) (All2i_cons r0 a) (All2i_cons r2 b) e) = e)


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

Goals:
  
  A : Type
  B : Type
  R : nat → A → B → Type
  n : nat
  e : apply_noConfusion [] []
        (λ _ : True, apply_noConfusion [] [] (λ _ : True, True)) eq_refl
        eq_refl
  ============================
   (noConfusionHom_All2i_obligation_2 A B R n [] [] All2i_nil All2i_nil
      (noConfusionHom_All2i_obligation_1 A B R n [] [] All2i_nil All2i_nil e) =
    e)

  
  A : Type
  B : Type
  R : nat → A → B → Type
  n : nat
  x : A
  y : B
  l : list A
  r : list B
  r0 : R n x y
  a : All2i R (S n) l r
  r2 : R n x y
  b : All2i R (S n) l r
  e : apply_noConfusion (x :: l) (x :: l)
        (DepElim.eq_simplification_sigma1 x x l l
           (λ H : x = x,
              DepElim.solution_left x
                (λ (y0 : B) (l0 : list A) (r1 : list B) 
                   (y1 : R n x y0) (a0 : All2i R (S n) l0 r1) 
                   (H0 : l0 = l),
                   DepElim.solution_left l
                     (λ (r2 : list B) (y2 : R n x y0) 
                        (a1 : All2i R (S n) l r2),
                        apply_noConfusion (y0 :: r2) 
                          (y :: r)
                          (DepElim.eq_simplification_sigma1 y0 y r2 r
                             (λ H1 : y0 = y,
                                DepElim.solution_left y
                                  (λ (r3 : list B) 
                                     (y3 : R n x y) 
                                     (a2 : All2i R (S n) l r3) 
                                     (H2 : r3 = r),
                                     DepElim.solution_left r
                                       (λ (y4 : R n x y) 
                                          (a3 : All2i R (S n) l r),
                                          {| pr1 := r0; pr2 := a |} =
                                          {| pr1 := y4; pr2 := a3 |}) r3 H2
                                       y3 a2) y0 H1 r2 y2 a1))) l0 H0 r1 y1
                     a0) x H y l r r2 b)) eq_refl eq_refl
  ============================
   (noConfusionHom_All2i_obligation_2 A B R n (x :: l) 
      (y :: r) (All2i_cons r0 a) (All2i_cons r2 b)
      (noConfusionHom_All2i_obligation_1 A B R n (x :: l) 
         (y :: r) (All2i_cons r0 a) (All2i_cons r2 b) e) = e)


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