Goal:
  
  ============================
   (∀ (A : Type) (P : A → Type) (a b : sigma (λ index : list A, All P index)) 
      (e : NoConfusion_All A P a b),
      (λ (A0 : Type) (P0 : A0 → Type) (a0
                                       b0 : sigma
                                              (λ index : list A0,
                                                 All P0 index)) 
         (H : a0 = b0), noConfusion_All_obligation_2 A0 P0 a0 b0 H) A P a b
        ((λ (A0 : Type) (P0 : A0 → Type) (a0
                                          b0 : sigma
                                                 (λ index : list A0,
                                                 All P0 index)) 
            (H : NoConfusion_All A0 P0 a0 b0),
            noConfusion_All_obligation_1 A0 P0 a0 b0 H) A P a b e) = e)


DEBUG:Going to execute:
Init.solve_noconf