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


DEBUG:Going to execute:
Init.solve_noconf