Goal:
  
  ============================
   (∀ (A : Type) (P : list A → A → Type) (l : list A) 
      (a b : All_fold P l) (e : NoConfusionHom_All_fold A P l a b),
      (λ (A0 : Type) (P0 : list A0 → A0 → Type) (l0 : list A0) 
         (a0 b0 : All_fold P0 l0) (H : a0 = b0),
         noConfusionHom_All_fold_obligation_2 A0 P0 l0 a0 b0 H) A P l a b
        ((λ (A0 : Type) (P0 : list A0 → A0 → Type) 
            (l0 : list A0) (a0 b0 : All_fold P0 l0) 
            (H : NoConfusionHom_All_fold A0 P0 l0 a0 b0),
            noConfusionHom_All_fold_obligation_1 A0 P0 l0 a0 b0 H) A P l a b
           e) = e)


DEBUG:Going to execute:
simpl; intros;
            match goal with
            | H:_ = _ |- _ = _ => try solve_noconf_hom_inv_equiv
            | H:_ = _ |- _ => try solve_noconf_prf
            | |- _ = _ => try solve_noconf_hom_inv
            end