Goal:
  
  ============================
   (∀ (A B : Type) (R : A → B → Type) (R' : ∀ (a : A) (b : B), R a b → Type) 
      (xs : list A) (ys : list B) (a : All2 R xs ys) 
      (a0 b : All2_dep R' a) (e : NoConfusionHom_All2_dep A B R R' xs ys a a0
                                    b),
      (λ (A0 B0 : Type) (R0 : A0 → B0 → Type) (R'0 : 
                                               ∀ (a1 : A0) (b0 : B0),
                                                 R0 a1 b0 → Type) 
         (xs0 : list A0) (ys0 : list B0) (a1 : All2 R0 xs0 ys0) 
         (a2 b0 : All2_dep R'0 a1) (H : a2 = b0),
         noConfusionHom_All2_dep_obligation_2 A0 B0 R0 R'0 xs0 ys0 a1 a2 b0 H)
        A B R R' xs ys a a0 b
        ((λ (A0 B0 : Type) (R0 : A0 → B0 → Type) (R'0 : 
                                                 ∀ (a1 : A0) (b0 : B0),
                                                 R0 a1 b0 → Type) 
            (xs0 : list A0) (ys0 : list B0) (a1 : All2 R0 xs0 ys0) 
            (a2 b0 : All2_dep R'0 a1) (H : NoConfusionHom_All2_dep A0 B0 R0
                                             R'0 xs0 ys0 a1 a2 b0),
            noConfusionHom_All2_dep_obligation_1 A0 B0 R0 R'0 xs0 ys0 a1 a2
              b0 H) A B R R' xs ys a a0 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