Goal:
  
  A : Type
  P : list A → list A → A → A → Type
  d : A
  d' : A
  Γ : list A
  Γ' : list A
  a : All2_fold P Γ Γ'
  p : P Γ Γ' d d'
  d0 : A
  d'0 : A
  Γ0 : list A
  Γ'0 : list A
  b : All2_fold P Γ0 Γ'0
  p0 : P Γ0 Γ'0 d0 d'0
  H : {|
        pr1 := d;
        pr2 :=
          {|
            pr1 := d';
            pr2 :=
              {|
                pr1 := Γ;
                pr2 := {| pr1 := Γ'; pr2 := {| pr1 := a; pr2 := p |} |}
              |}
          |}
      |} =
      {|
        pr1 := d0;
        pr2 :=
          {|
            pr1 := d'0;
            pr2 :=
              {|
                pr1 := Γ0;
                pr2 := {| pr1 := Γ'0; pr2 := {| pr1 := b; pr2 := p0 |} |}
              |}
          |}
      |}
  ============================
   ({|
      pr1 := {| pr1 := d :: Γ; pr2 := d' :: Γ' |};
      pr2 := All2_fold_cons P a p
    |} =
    {|
      pr1 := {| pr1 := d0 :: Γ0; pr2 := d'0 :: Γ'0 |};
      pr2 := All2_fold_cons P b p0
    |})


DEBUG:Going to execute:
let rhs := fresh in
           set (rhs := y) in *; pattern sigma rhs; clearbody rhs; destruct H;
            simpl
DEBUG LTAC Evaluated term: H
DEBUG LTAC Evaluated term: ({|
                              pr1 := d;
                              pr2 :=
                                {|
                                  pr1 := d';
                                  pr2 :=
                                    {|
                                      pr1 := Γ;
                                      pr2 :=
                                        {|
                                          pr1 := Γ';
                                          pr2 := {| pr1 := a; pr2 := p |}
                                        |}
                                    |}
                                |}
                            |} =
                            {|
                              pr1 := d0;
                              pr2 :=
                                {|
                                  pr1 := d'0;
                                  pr2 :=
                                    {|
                                      pr1 := Γ0;
                                      pr2 :=
                                        {|
                                          pr1 := Γ'0;
                                          pr2 := {| pr1 := b; pr2 := p0 |}
                                        |}
                                    |}
                                |}
                            |})
Level 6: type of H
 has value 
({|
   pr1 := d;
   pr2 :=
     {|
       pr1 := d';
       pr2 :=
         {|
           pr1 := Γ; pr2 := {| pr1 := Γ'; pr2 := {| pr1 := a; pr2 := p |} |}
         |}
     |}
 |} =
 {|
   pr1 := d0;
   pr2 :=
     {|
       pr1 := d'0;
       pr2 :=
         {|
           pr1 := Γ0;
           pr2 := {| pr1 := Γ'0; pr2 := {| pr1 := b; pr2 := p0 |} |}
         |}
     |}
 |})