Goal:
  
  ============================
   (∀ (A : Type) (P : A → Type) (a b : sigma (λ index : list A, All P index)),
      NoConfusion_All A P a b → a = b)


DEBUG:Going to execute:
Init.solve_noconf