Goal:
  
  ============================
   (∀ (A : Type) (P : nat → A → A → Type) (a
                                           b : sigma
                                                 (λ index : 
                                                 sigma
                                                 (λ _ : nat,
                                                 sigma (λ _ : list A, list A)),
                                                 OnOne2i P 
                                                 (pr1 index)
                                                 (pr1 (pr2 index))
                                                 (pr2 (pr2 index)))) 
      (e : NoConfusion_OnOne2i A P a b),
      noConfusion_OnOne2i_obligation_2 A P a b
        (noConfusion_OnOne2i_obligation_1 A P a b e) = e)


DEBUG:Going to execute:
intros