Goal:
  
  A : Type
  B : Type
  R : A → B → Type
  R' : ∀ (a : A) (b : B), R a b → Type
  x : A
  y : B
  l : list A
  l' : list B
  r : R x y
  rs : All2 R l l'
  r0 : R' x y r
  a0 : All2_dep R' rs
  b0 : All2_dep R' (All2_cons r rs)
  x0 : A
  y0 : B
  l0 : list A
  l'0 : list B
  r1 : R x0 y0
  rs0 : All2 R l0 l'0
  r2 : R' x0 y0 r1
  b : All2_dep R' rs0
  ============================
   ({|
      pr1 :=
        {|
          pr1 := x :: l; pr2 := {| pr1 := y :: l'; pr2 := All2_cons r rs |}
        |};
      pr2 := b0
    |} =
    {|
      pr1 :=
        {|
          pr1 := x0 :: l0;
          pr2 := {| pr1 := y0 :: l'0; pr2 := All2_cons r1 rs0 |}
        |};
      pr2 := All2_dep_cons r2 b
    |}
    → ∀ (H := CoreTactics.block) (e : NoConfusionHom_All2_dep A B R R'
                                        (x :: l) (y :: l') 
                                        (All2_cons r rs)
                                        (All2_dep_cons r0 a0) b0),
        let H0 := CoreTactics.block in
        noConfusionHom_All2_dep_obligation_2 A B R R' 
          (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0) b0
          (noConfusionHom_All2_dep_obligation_1 A B R R' 
             (x :: l) (y :: l') (All2_cons r rs) (All2_dep_cons r0 a0) b0 e) =
        e)


DEBUG:Going to execute:
match goal with
           | |- context [ eq_rect_r _ _ eq_refl ] => progress simpl eq_rect_r
           | |- context [ eq_rect _ _ _ _ eq_refl ] => progress simpl eq_rect
           | |- context [ Prop.Logic.transport _ eq_refl _ ] =>
                 progress simpl Prop.Logic.transport
           | |- context [ Logic.eq_elim _ _ _ _ _ eq_refl ] =>
                 progress simpl eq_rect
           | |- context [ Logic.eq_elim_r _ _ _ _ eq_refl ] =>
                 progress simpl Logic.eq_elim_r
           | |- context [ noConfusion_inv _ ] =>
                 progress simpl noConfusion_inv
           | |- DepElim.opaque_ind_pack_eq_inv ?G eq_refl =>
                 apply (DepElim.simplify_ind_pack_inv B x p G)
           | |- let _ := CoreTactics.block in _ => fail 1
           | |- _ => simplify * || simplify ?; cbv beta
           | |- _ → ?B =>
                 let ty := type of B in
                 intro || (let H := fresh in
                           intro
                           H)
           | |- ∀ x, _ => let H := fresh x in
                          intro
                          H
           | |- _ => intro
           end