Goal:
  
  ============================
   (∀ (A B : Type) (R : A → B → Type) (l0 : list A) 
      (l : list B) (a b : All2 R l0 l) (e : NoConfusionHom_All2 A B R l0 l a
                                              b),
      (λ (A0 B0 : Type) (R0 : A0 → B0 → Type) (l1 : list A0) 
         (l2 : list B0) (a0 b0 : All2 R0 l1 l2) (H : a0 = b0),
         noConfusionHom_All2_obligation_2 A0 B0 R0 l1 l2 a0 b0 H) A B R l0 l
        a b
        ((λ (A0 B0 : Type) (R0 : A0 → B0 → Type) (l1 : list A0) 
            (l2 : list B0) (a0 b0 : All2 R0 l1 l2) 
            (H : NoConfusionHom_All2 A0 B0 R0 l1 l2 a0 b0),
            noConfusionHom_All2_obligation_1 A0 B0 R0 l1 l2 a0 b0 H) A B R l0
           l a b e) = e)


DEBUG:Going to execute:
Init.solve_noconf_hom