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


DEBUG:Going to execute:
Init.solve_noconf_hom