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:
simpl; DepElim.hnf_eq