Goal:
  
  A : Type
  B : Type
  R : nat → A → B → Type
  n : nat
  x : A
  y : B
  l : list A
  r : list B
  r0 : R n x y
  a : All2i R (S n) l r
  r2 : R n x y
  b : All2i R (S n) l r
  H : apply_noConfusion (x :: l) (x :: l)
        (DepElim.eq_simplification_sigma1 x x l l
           (λ H : x = x,
              DepElim.solution_left x
                (λ (y0 : B) (l0 : list A) (r1 : list B) 
                   (y1 : R n x y0) (a0 : All2i R (S n) l0 r1) 
                   (H0 : l0 = l),
                   DepElim.solution_left l
                     (λ (r2 : list B) (y2 : R n x y0) 
                        (a1 : All2i R (S n) l r2),
                        apply_noConfusion (y0 :: r2) 
                          (y :: r)
                          (DepElim.eq_simplification_sigma1 y0 y r2 r
                             (λ H1 : y0 = y,
                                DepElim.solution_left y
                                  (λ (r3 : list B) 
                                     (y3 : R n x y) 
                                     (a2 : All2i R (S n) l r3) 
                                     (H2 : r3 = r),
                                     DepElim.solution_left r
                                       (λ (y4 : R n x y) 
                                          (a3 : All2i R (S n) l r),
                                          {| pr1 := r0; pr2 := a |} =
                                          {| pr1 := y4; pr2 := a3 |}) r3 H2
                                       y3 a2) y0 H1 r2 y2 a1))) l0 H0 r1 y1
                     a0) x H y l r r2 b)) eq_refl eq_refl
  ============================
   (All2i_cons r0 a = All2i_cons r2 b)


DEBUG:Going to execute:
hnf in id
Level 5: evaluation returns
hnf in id; CoreTactics.destruct_tele_eq id || DepElim.depelim id
where
id := H
of type
constr
b := b
of type
constr
a := a
of type
constr
R := eq
of type
constr of type tacvalue