Goal:
  
  ============================
   (∀ (A : Type) (P : list A → list A → A → A → Type) 
      (a
       b : sigma
             (λ index : sigma (λ _ : list A, list A),
                All2_fold P (pr1 index) (pr2 index))) 
      (e : a = b),
      (λ (A0 : Type) (P0 : list A0 → list A0 → A0 → A0 → Type) 
         (a0
          b0 : sigma
                 (λ index : sigma (λ _ : list A0, list A0),
                    All2_fold P0 (pr1 index) (pr2 index))) 
         (H : NoConfusion_All2_fold A0 P0 a0 b0),
         noConfusion_All2_fold_obligation_1 A0 P0 a0 b0 H) A P a b
        ((λ (A0 : Type) (P0 : list A0 → list A0 → A0 → A0 → Type) 
            (a0
             b0 : sigma
                    (λ index : sigma (λ _ : list A0, list A0),
                       All2_fold P0 (pr1 index) (pr2 index))) 
            (H : a0 = b0), noConfusion_All2_fold_obligation_2 A0 P0 a0 b0 H)
           A P a b e) = e)


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