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:
let y' := eval hnf in y in
           change_no_check (x' = y')
DEBUG LTAC Evaluated term: (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)
DEBUG LTAC Evaluated term: eq_refl