Goal:
  
  ============================
   (∀ (A B : Type) (P : B → A → A → Type) (a
                                           b : sigma
                                                 (λ index : 
                                                 sigma
                                                 (λ _ : list B,
                                                 sigma (λ _ : list A, list A)),
                                                 OnOne2All P 
                                                 (pr1 index)
                                                 (pr1 (pr2 index))
                                                 (pr2 (pr2 index)))) 
      (e : NoConfusion_OnOne2All A B P a b),
      (λ (A0 B0 : Type) (P0 : B0 → A0 → A0 → Type) 
         (a0
          b0 : sigma
                 (λ index : sigma
                              (λ _ : list B0, sigma (λ _ : list A0, list A0)),
                    OnOne2All P0 (pr1 index) (pr1 (pr2 index))
                      (pr2 (pr2 index)))) (H : a0 = b0),
         noConfusion_OnOne2All_obligation_2 A0 B0 P0 a0 b0 H) A B P a b
        ((λ (A0 B0 : Type) (P0 : B0 → A0 → A0 → Type) 
            (a0
             b0 : sigma
                    (λ index : sigma
                                 (λ _ : list B0,
                                    sigma (λ _ : list A0, list A0)),
                       OnOne2All P0 (pr1 index) (pr1 (pr2 index))
                         (pr2 (pr2 index)))) (H : 
                                              NoConfusion_OnOne2All A0 B0 P0
                                                a0 b0),
            noConfusion_OnOne2All_obligation_1 A0 B0 P0 a0 b0 H) A B 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