Goal:
    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)


DEBUG:Going to execute:
repeat (simpl; DepElim.hnf_eq; DepElim.rewrite_refl_id)