Goal:
  
  ============================
   (∀ (A : Type) (P : nat → A → Type) (n : nat) (l : list A) 
      (a b : Alli P n l), NoConfusionHom_Alli A P n l a b → a = b)


DEBUG:Going to execute:
Init.solve_noconf_hom