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
  ============================
   (let H := CoreTactics.block in
    noConfusionHom_All2i_obligation_1 A B R n (x :: l) 
      (y :: r) (All2i_cons r0 a) (All2i_cons r0 a)
      (noConfusionHom_All2i_obligation_2 A B R n (x :: l) 
         (y :: r) (All2i_cons r0 a) (All2i_cons r0 a) eq_refl) = eq_refl)


DEBUG:Going to execute:
intros _

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

  
  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
  ============================
   (noConfusionHom_All2i_obligation_1 A B R n (x :: l) 
      (y :: r) (All2i_cons r0 a) (All2i_cons r0 a)
      (noConfusionHom_All2i_obligation_2 A B R n (x :: l) 
         (y :: r) (All2i_cons r0 a) (All2i_cons r0 a) eq_refl) = eq_refl)


DEBUG:Going to execute:
CoreTactics.unblock_goal

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

  
  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
  ============================
   (noConfusionHom_All2i_obligation_1 A B R n (x :: l) 
      (y :: r) (All2i_cons r0 a) (All2i_cons r0 a)
      (noConfusionHom_All2i_obligation_2 A B R n (x :: l) 
         (y :: r) (All2i_cons r0 a) (All2i_cons r0 a) eq_refl) = eq_refl)


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

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

  
  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
  ============================
   (noConfusionHom_All2i_obligation_1 A B R n (x :: l) 
      (y :: r) (All2i_cons r0 a) (All2i_cons r0 a)
      (noConfusionHom_All2i_obligation_2 A B R n (x :: l) 
         (y :: r) (All2i_cons r0 a) (All2i_cons r0 a) eq_refl) = eq_refl)


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

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

  
  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
  ============================
   (noConfusionHom_All2i_obligation_1 A B R n (x :: l) 
      (y :: r) (All2i_cons r0 a) (All2i_cons r0 a)
      (noConfusionHom_All2i_obligation_2 A B R n (x :: l) 
         (y :: r) (All2i_cons r0 a) (All2i_cons r0 a) eq_refl) = eq_refl)


DEBUG:Going to execute:
cbv zeta

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

  
  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
  ============================
   (noConfusionHom_All2i_obligation_1 A B R n (x :: l) 
      (y :: r) (All2i_cons r0 a) (All2i_cons r0 a)
      (noConfusionHom_All2i_obligation_2 A B R n (x :: l) 
         (y :: r) (All2i_cons r0 a) (All2i_cons r0 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  R : nat → A → B → Type  n : nat
  ============================
   (apply_noConfusion [] []
      (Logic.True_rect_dep
         (λ H : True,
            ∀ e : [] = [],
              eq_rect {| pr1 := n; pr2 := {| pr1 := []; pr2 := [] |} |}
                (λ index : sigma (λ _ : nat, sigma (λ _ : list A, list B)),
                   All2i R (pr1 index) (pr1 (pr2 index)) (pr2 (pr2 index)))
                All2i_nil {| pr1 := n; pr2 := {| pr1 := []; pr2 := [] |} |}
                match
                  DepElim.pack_sigma_eq_nondep
                    match H with
                    | I => eq_refl
                    end e in (_ = p)
                  return
                    ({| pr1 := n; pr2 := {| pr1 := []; pr2 := [] |} |} =
                     {| pr1 := n; pr2 := p |})
                with
                | eq_refl => eq_refl
                end = All2i_nil
              → apply_noConfusion [] []
                  (λ _ : True, apply_noConfusion [] [] (λ _ : True, True))
                  eq_refl eq_refl → All2i_nil = All2i_nil)
         (apply_noConfusion [] []
            (Logic.True_rect_dep
               (λ H : True,
                  eq_rect {| pr1 := n; pr2 := {| pr1 := []; pr2 := [] |} |}
                    (λ index : sigma
                                 (λ _ : nat, sigma (λ _ : list A, list B)),
                       All2i R (pr1 index) (pr1 (pr2 index))
                         (pr2 (pr2 index))) All2i_nil
                    {| pr1 := n; 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 := n; pr2 := {| pr1 := []; pr2 := [] |} |} =
                         {| pr1 := n; pr2 := p |})
                    with
                    | eq_refl => eq_refl
                    end = All2i_nil
                  → apply_noConfusion [] []
                      (λ _ : True, apply_noConfusion [] [] (λ _ : True, True))
                      eq_refl eq_refl → All2i_nil = All2i_nil)
               (λ H : All2i_nil = All2i_nil,
                  DepElim.solution_left All2i_nil
                    (λ H0 : apply_noConfusion [] []
                              (λ _ : True,
                                 apply_noConfusion [] [] (λ _ : True, True))
                              eq_refl eq_refl,
                       match H0 with
                       | I => eq_refl
                       end) All2i_nil H)))) eq_refl eq_refl eq_refl I =
    eq_refl)

  
  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
  ============================
   (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) (r1 : list B) 
                 (r2 : R n x y0) (b : All2i R (S n) l0 r1) 
                 (e : l = l0),
                 DepElim.solution_right_dep l
                   (λ (r3 : list B) (r4 : R n x y0) (b0 : All2i R (S n) l r3),
                      apply_noConfusion (y :: r) (y0 :: r3)
                        (DepElim.eq_simplification_sigma1_nondep_dep y y0 r
                           r3
                           (λ e'0 : y = y0,
                              DepElim.solution_right_dep y
                                (λ (r5 : list B) (r6 : R n x y) 
                                   (b1 : All2i R (S n) l r5) 
                                   (e0 : r = r5),
                                   DepElim.solution_right_dep r
                                     (λ (r7 : R n x y) 
                                        (b2 : All2i R (S n) l r) 
                                        (H : All2i_cons r0 a =
                                             All2i_cons r7 b2),
                                        DepElim.solution_left
                                          (All2i_cons r7 b2)
                                          (λ H0 : 
                                              apply_noConfusion 
                                                (x :: l) 
                                                (x :: l)
                                                (DepElim.eq_simplification_sigma1
                                                 x x l l
                                                 (λ H0 : x = x,
                                                 DepElim.solution_left x
                                                 (λ (y1 : B) 
                                                 (l1 : list A) 
                                                 (r8 : list B) 
                                                 (y2 : 
                                                 R n x y1) 
                                                 (a0 : 
                                                 All2i R (S n) l1 r8) 
                                                 (H1 : 
                                                 l1 = l),
                                                 DepElim.solution_left l
                                                 (λ (r9 : list B) 
                                                 (y3 : 
                                                 R n x y1) 
                                                 (a1 : 
                                                 All2i R (S n) l r9),
                                                 apply_noConfusion 
                                                 (y1 :: r9) 
                                                 (y :: r)
                                                 (DepElim.eq_simplification_sigma1
                                                 y1 y r9 r
                                                 (λ H2 : y1 = y,
                                                 DepElim.solution_left y
                                                 (λ (r10 : list B) 
                                                 (y4 : 
                                                 R n x y) 
                                                 (a2 : 
                                                 All2i R (S n) l r10) 
                                                 (H3 : 
                                                 r10 = r),
                                                 DepElim.solution_left r
                                                 (λ (y5 : R n x y) 
                                                 (a3 : 
                                                 All2i R (S n) l r),
                                                 {| pr1 := r0; pr2 := a |} =
                                                 {| pr1 := y5; pr2 := a3 |})
                                                 r10 H3 y4 a2) y1 H2 r9 y3 a1)))
                                                 l1 H1 r8 y2 a0) x H0 y l r
                                                 r7 b2)) eq_refl eq_refl,
                                             match
                                               H0 in (_ = s)
                                               return
                                                 (All2i_cons r0 a =
                                                 All2i_cons (pr1 s) (pr2 s))
                                             with
                                             | eq_refl => eq_refl
                                             end) 
                                          (All2i_cons r0 a) H) r5 e0 r6 b1)
                                y0 e'0 r3 r4 b0))) l0 e r1 r2 b) x e' y l r
              r0 a)) eq_refl eq_refl eq_refl eq_refl = eq_refl)


DEBUG:Going to execute:
DepElim.simpl_equations

Goals:
    A : Type  B : Type  R : nat → A → B → Type  n : nat
  ============================
   (apply_noConfusion [] []
      (Logic.True_rect_dep
         (λ H : True,
            ∀ e : [] = [],
              eq_rect {| pr1 := n; pr2 := {| pr1 := []; pr2 := [] |} |}
                (λ index : sigma (λ _ : nat, sigma (λ _ : list A, list B)),
                   All2i R (pr1 index) (pr1 (pr2 index)) (pr2 (pr2 index)))
                All2i_nil {| pr1 := n; pr2 := {| pr1 := []; pr2 := [] |} |}
                match
                  DepElim.pack_sigma_eq_nondep
                    match H with
                    | I => eq_refl
                    end e in (_ = p)
                  return
                    ({| pr1 := n; pr2 := {| pr1 := []; pr2 := [] |} |} =
                     {| pr1 := n; pr2 := p |})
                with
                | eq_refl => eq_refl
                end = All2i_nil
              → apply_noConfusion [] []
                  (λ _ : True, apply_noConfusion [] [] (λ _ : True, True))
                  eq_refl eq_refl → All2i_nil = All2i_nil)
         (apply_noConfusion [] []
            (Logic.True_rect_dep
               (λ H : True,
                  eq_rect {| pr1 := n; pr2 := {| pr1 := []; pr2 := [] |} |}
                    (λ index : sigma
                                 (λ _ : nat, sigma (λ _ : list A, list B)),
                       All2i R (pr1 index) (pr1 (pr2 index))
                         (pr2 (pr2 index))) All2i_nil
                    {| pr1 := n; 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 := n; pr2 := {| pr1 := []; pr2 := [] |} |} =
                         {| pr1 := n; pr2 := p |})
                    with
                    | eq_refl => eq_refl
                    end = All2i_nil
                  → apply_noConfusion [] []
                      (λ _ : True, apply_noConfusion [] [] (λ _ : True, True))
                      eq_refl eq_refl → All2i_nil = All2i_nil)
               (λ H : All2i_nil = All2i_nil,
                  DepElim.solution_left All2i_nil
                    (λ H0 : apply_noConfusion [] []
                              (λ _ : True,
                                 apply_noConfusion [] [] (λ _ : True, True))
                              eq_refl eq_refl,
                       match H0 with
                       | I => eq_refl
                       end) All2i_nil H)))) eq_refl eq_refl eq_refl I =
    eq_refl)

  
  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
  ============================
   (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) (r1 : list B) 
                 (r2 : R n x y0) (b : All2i R (S n) l0 r1) 
                 (e : l = l0),
                 DepElim.solution_right_dep l
                   (λ (r3 : list B) (r4 : R n x y0) (b0 : All2i R (S n) l r3),
                      apply_noConfusion (y :: r) (y0 :: r3)
                        (DepElim.eq_simplification_sigma1_nondep_dep y y0 r
                           r3
                           (λ e'0 : y = y0,
                              DepElim.solution_right_dep y
                                (λ (r5 : list B) (r6 : R n x y) 
                                   (b1 : All2i R (S n) l r5) 
                                   (e0 : r = r5),
                                   DepElim.solution_right_dep r
                                     (λ (r7 : R n x y) 
                                        (b2 : All2i R (S n) l r) 
                                        (H : All2i_cons r0 a =
                                             All2i_cons r7 b2),
                                        DepElim.solution_left
                                          (All2i_cons r7 b2)
                                          (λ H0 : 
                                              apply_noConfusion 
                                                (x :: l) 
                                                (x :: l)
                                                (DepElim.eq_simplification_sigma1
                                                 x x l l
                                                 (λ H0 : x = x,
                                                 DepElim.solution_left x
                                                 (λ (y1 : B) 
                                                 (l1 : list A) 
                                                 (r8 : list B) 
                                                 (y2 : 
                                                 R n x y1) 
                                                 (a0 : 
                                                 All2i R (S n) l1 r8) 
                                                 (H1 : 
                                                 l1 = l),
                                                 DepElim.solution_left l
                                                 (λ (r9 : list B) 
                                                 (y3 : 
                                                 R n x y1) 
                                                 (a1 : 
                                                 All2i R (S n) l r9),
                                                 apply_noConfusion 
                                                 (y1 :: r9) 
                                                 (y :: r)
                                                 (DepElim.eq_simplification_sigma1
                                                 y1 y r9 r
                                                 (λ H2 : y1 = y,
                                                 DepElim.solution_left y
                                                 (λ (r10 : list B) 
                                                 (y4 : 
                                                 R n x y) 
                                                 (a2 : 
                                                 All2i R (S n) l r10) 
                                                 (H3 : 
                                                 r10 = r),
                                                 DepElim.solution_left r
                                                 (λ (y5 : R n x y) 
                                                 (a3 : 
                                                 All2i R (S n) l r),
                                                 {| pr1 := r0; pr2 := a |} =
                                                 {| pr1 := y5; pr2 := a3 |})
                                                 r10 H3 y4 a2) y1 H2 r9 y3 a1)))
                                                 l1 H1 r8 y2 a0) x H0 y l r
                                                 r7 b2)) eq_refl eq_refl,
                                             match
                                               H0 in (_ = s)
                                               return
                                                 (All2i_cons r0 a =
                                                 All2i_cons (pr1 s) (pr2 s))
                                             with
                                             | eq_refl => eq_refl
                                             end) 
                                          (All2i_cons r0 a) H) r5 e0 r6 b1)
                                y0 e'0 r3 r4 b0))) l0 e r1 r2 b) x e' y l r
              r0 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)