Goal:
    A : Type  B : Type  C : Type  R : A → B → C → Type
  ============================
   (apply_noConfusion [] []
      (Logic.True_rect_dep
         (λ H : True,
            ∀ e : {| pr1 := []; pr2 := [] |} = {| pr1 := []; pr2 := [] |},
              eq_rect {| pr1 := []; pr2 := {| pr1 := []; pr2 := [] |} |}
                (λ index : sigma (λ _ : list A, sigma (λ _ : list B, list C)),
                   All3 R (pr1 index) (pr1 (pr2 index)) (pr2 (pr2 index)))
                All3_nil {| pr1 := []; pr2 := {| pr1 := []; pr2 := [] |} |}
                (DepElim.pack_sigma_eq_nondep match H with
                                              | I => eq_refl
                                              end e) = All3_nil
              → apply_noConfusion [] []
                  (λ _ : True,
                     DepElim.eq_simplification_sigma1 [] [] [] []
                       (apply_noConfusion [] []
                          (λ _ : True,
                             apply_noConfusion [] [] (λ _ : True, True))))
                  eq_refl eq_refl → All3_nil = All3_nil)
         (DepElim.eq_simplification_sigma1_nondep_dep [] [] [] []
            (apply_noConfusion [] []
               (Logic.True_rect_dep
                  (λ H : True,
                     ∀ e : [] = [],
                       eq_rect
                         {| pr1 := []; pr2 := {| pr1 := []; pr2 := [] |} |}
                         (λ index : sigma
                                      (λ _ : list A,
                                         sigma (λ _ : list B, list C)),
                            All3 R (pr1 index) (pr1 (pr2 index))
                              (pr2 (pr2 index))) All3_nil
                         {| pr1 := []; pr2 := {| pr1 := []; pr2 := [] |} |}
                         match
                           DepElim.pack_sigma_eq_nondep
                             match H with
                             | I => eq_refl
                             end e in (_ = p)
                           return
                             ({|
                                pr1 := []; pr2 := {| pr1 := []; pr2 := [] |}
                              |} = {| pr1 := []; pr2 := p |})
                         with
                         | eq_refl => eq_refl
                         end = All3_nil
                       → apply_noConfusion [] []
                           (λ _ : True,
                              DepElim.eq_simplification_sigma1 [] [] [] []
                                (apply_noConfusion [] []
                                   (λ _ : True,
                                      apply_noConfusion [] []
                                        (λ _ : True, True)))) eq_refl eq_refl
                         → All3_nil = All3_nil)
                  (apply_noConfusion [] []
                     (Logic.True_rect_dep
                        (λ H : True,
                           eq_rect
                             {|
                               pr1 := []; pr2 := {| pr1 := []; pr2 := [] |}
                             |}
                             (λ index : sigma
                                          (λ _ : list A,
                                             sigma (λ _ : list B, list C)),
                                All3 R (pr1 index) 
                                  (pr1 (pr2 index)) 
                                  (pr2 (pr2 index))) All3_nil
                             {|
                               pr1 := []; 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 := [];
                                    pr2 := {| pr1 := []; pr2 := [] |}
                                  |} = {| pr1 := []; pr2 := p |})
                             with
                             | eq_refl => eq_refl
                             end = All3_nil
                           → apply_noConfusion [] []
                               (λ _ : True,
                                  DepElim.eq_simplification_sigma1 [] [] []
                                    []
                                    (apply_noConfusion [] []
                                       (λ _ : True,
                                          apply_noConfusion [] []
                                            (λ _ : True, True)))) eq_refl
                               eq_refl → All3_nil = All3_nil)
                        (λ H : All3_nil = All3_nil,
                           DepElim.solution_left All3_nil
                             (λ H0 : apply_noConfusion [] []
                                       (λ _ : True,
                                          DepElim.eq_simplification_sigma1 []
                                            [] [] []
                                            (apply_noConfusion [] []
                                               (λ _ : True,
                                                 apply_noConfusion [] []
                                                 (λ _ : True, True))))
                                       eq_refl eq_refl,
                                match H0 with
                                | I => eq_refl
                                end) All3_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 : {| pr1 := []; pr2 := [] |} =
                                          {| pr1 := []; pr2 := [] |},
                                      eq_rect
                                        {|
                                          pr1 := [];
                                          pr2 := {| pr1 := []; pr2 := [] |}
                                        |}
                                        (λ index : 
                                            sigma
                                              (λ _ : list A,
                                                 sigma (λ _ : list B, list C)),
                                           All3 R 
                                             (pr1 index) 
                                             (pr1 (pr2 index))
                                             (pr2 (pr2 index))) All3_nil
                                        {|
                                          pr1 := [];
                                          pr2 := {| pr1 := []; pr2 := [] |}
                                        |}
                                        (DepElim.pack_sigma_eq_nondep
                                           match H with
                                           | I => eq_refl
                                           end e) = All3_nil
                                      → apply_noConfusion [] []
                                          (λ _ : True,
                                             DepElim.eq_simplification_sigma1
                                               [] [] [] []
                                               (apply_noConfusion [] []
                                                 (λ _ : True,
                                                 apply_noConfusion [] []
                                                 (λ _ : True, True))))
                                          eq_refl eq_refl
                                        → All3_nil = All3_nil)
                                 (DepElim.eq_simplification_sigma1_nondep_dep
                                    [] [] [] []
                                    (apply_noConfusion [] []
                                       (Logic.True_rect_dep
                                          (λ H : True,
                                             ∀ e : [] = [],
                                               eq_rect
                                                 {|
                                                 pr1 := [];
                                                 pr2 :=
                                                 {| pr1 := []; pr2 := [] |}
                                                 |}
                                                 (λ index : 
                                                 sigma
                                                 (λ _ : list A,
                                                 sigma (λ _ : list B, list C)),
                                                 All3 R 
                                                 (pr1 index)
                                                 (pr1 (pr2 index))
                                                 (pr2 (pr2 index))) All3_nil
                                                 {|
                                                 pr1 := [];
                                                 pr2 :=
                                                 {| pr1 := []; pr2 := [] |}
                                                 |}
                                                 match
                                                 DepElim.pack_sigma_eq_nondep
                                                 match H with
                                                 | I => eq_refl
                                                 end e in 
                                                 (_ = p)
                                                 return
                                                 ({|
                                                 pr1 := [];
                                                 pr2 :=
                                                 {| pr1 := []; pr2 := [] |}
                                                 |} =
                                                 {| pr1 := []; pr2 := p |})
                                                 with
                                                 | eq_refl => eq_refl
                                                 end = All3_nil
                                               → apply_noConfusion [] []
                                                 (λ _ : True,
                                                 DepElim.eq_simplification_sigma1
                                                 [] [] [] []
                                                 (apply_noConfusion [] []
                                                 (λ _ : True,
                                                 apply_noConfusion [] []
                                                 (λ _ : True, True))))
                                                 eq_refl eq_refl
                                                 → 
                                                 All3_nil = All3_nil)
                                          (apply_noConfusion [] []
                                             (Logic.True_rect_dep
                                                (λ H : True,
                                                 eq_rect
                                                 {|
                                                 pr1 := [];
                                                 pr2 :=
                                                 {| pr1 := []; pr2 := [] |}
                                                 |}
                                                 (λ index : 
                                                 sigma
                                                 (λ _ : list A,
                                                 sigma (λ _ : list B, list C)),
                                                 All3 R 
                                                 (pr1 index)
                                                 (pr1 (pr2 index))
                                                 (pr2 (pr2 index))) All3_nil
                                                 {|
                                                 pr1 := [];
                                                 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 := [];
                                                 pr2 :=
                                                 {| pr1 := []; pr2 := [] |}
                                                 |} =
                                                 {| pr1 := []; pr2 := p |})
                                                 with
                                                 | eq_refl => eq_refl
                                                 end = All3_nil
                                                 → 
                                                 apply_noConfusion [] []
                                                 (λ _ : True,
                                                 DepElim.eq_simplification_sigma1
                                                 [] [] [] []
                                                 (apply_noConfusion [] []
                                                 (λ _ : True,
                                                 apply_noConfusion [] []
                                                 (λ _ : True, True))))
                                                 eq_refl eq_refl
                                                 → 
                                                 All3_nil = All3_nil)
                                                (λ H : All3_nil = All3_nil,
                                                 DepElim.solution_left
                                                 All3_nil
                                                 (λ H0 : 
                                                 apply_noConfusion [] []
                                                 (λ _ : True,
                                                 DepElim.eq_simplification_sigma1
                                                 [] [] [] []
                                                 (apply_noConfusion [] []
                                                 (λ _ : True,
                                                 apply_noConfusion [] []
                                                 (λ _ : True, True))))
                                                 eq_refl eq_refl,
                                                 match H0 with
                                                 | I => eq_refl
                                                 end) All3_nil H)))))))
                              eq_refl eq_refl eq_refl I)
DEBUG LTAC Evaluated term: eq_refl