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:
match goal with
           | |- ?x = ?y =>
                 let x' := eval hnf in x in
                 let y' := eval hnf in y in
                 change_no_check (x' = y')
           end