Goal:
    A : Type  P : list A → A → Type
  ============================
   (apply_noConfusion [] []
      (Logic.True_rect_dep
         (λ H : True,
            rew [λ index : list A, All_fold P index]
                match H with
                | I => eq_refl
                end in All_fold_nil P = All_fold_nil P
            → apply_noConfusion [] [] (λ _ : True, True) eq_refl
              → All_fold_nil P = All_fold_nil P)
         (λ H : All_fold_nil P = All_fold_nil P,
            DepElim.solution_left (All_fold_nil P)
              (λ H0 : apply_noConfusion [] [] (λ _ : True, True) eq_refl,
                 match H0 with
                 | I => eq_refl
                 end) (All_fold_nil P) H)) 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,
                                    rew [λ index : list A, All_fold P index]
                                        match H with
                                        | I => eq_refl
                                        end in All_fold_nil P =
                                    All_fold_nil P
                                    → apply_noConfusion [] []
                                        (λ _ : True, True) eq_refl
                                      → All_fold_nil P = All_fold_nil P)
                                 (λ H : All_fold_nil P = All_fold_nil P,
                                    DepElim.solution_left 
                                      (All_fold_nil P)
                                      (λ H0 : apply_noConfusion [] []
                                                (λ _ : True, True) eq_refl,
                                         match H0 with
                                         | I => eq_refl
                                         end) (All_fold_nil P) H)) eq_refl
                              eq_refl I)
DEBUG LTAC Evaluated term: eq_refl