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
  ============================
   ({|
      pr1 := {| pr1 := d :: Γ; pr2 := d' :: Γ' |};
      pr2 := All2_fold_cons P a p
    |} =
    {|
      pr1 :=
        {|
          pr1 :=
            pr1
              {|
                pr1 := d;
                pr2 :=
                  {|
                    pr1 := d';
                    pr2 :=
                      {|
                        pr1 := Γ;
                        pr2 :=
                          {| pr1 := Γ'; pr2 := {| pr1 := a; pr2 := p |} |}
                      |}
                  |}
              |}
            :: pr1
                 (pr2
                    (pr2
                       {|
                         pr1 := d;
                         pr2 :=
                           {|
                             pr1 := d';
                             pr2 :=
                               {|
                                 pr1 := Γ;
                                 pr2 :=
                                   {|
                                     pr1 := Γ';
                                     pr2 := {| pr1 := a; pr2 := p |}
                                   |}
                               |}
                           |}
                       |}));
          pr2 :=
            pr1
              (pr2
                 {|
                   pr1 := d;
                   pr2 :=
                     {|
                       pr1 := d';
                       pr2 :=
                         {|
                           pr1 := Γ;
                           pr2 :=
                             {| pr1 := Γ'; pr2 := {| pr1 := a; pr2 := p |} |}
                         |}
                     |}
                 |})
            :: pr1
                 (pr2
                    (pr2
                       (pr2
                          {|
                            pr1 := d;
                            pr2 :=
                              {|
                                pr1 := d';
                                pr2 :=
                                  {|
                                    pr1 := Γ;
                                    pr2 :=
                                      {|
                                        pr1 := Γ';
                                        pr2 := {| pr1 := a; pr2 := p |}
                                      |}
                                  |}
                              |}
                          |})))
        |};
      pr2 :=
        All2_fold_cons P
          (pr1
             (pr2
                (pr2
                   (pr2
                      (pr2
                         {|
                           pr1 := d;
                           pr2 :=
                             {|
                               pr1 := d';
                               pr2 :=
                                 {|
                                   pr1 := Γ;
                                   pr2 :=
                                     {|
                                       pr1 := Γ';
                                       pr2 := {| pr1 := a; pr2 := p |}
                                     |}
                                 |}
                             |}
                         |})))))
          (pr2
             (pr2
                (pr2
                   (pr2
                      (pr2
                         {|
                           pr1 := d;
                           pr2 :=
                             {|
                               pr1 := d';
                               pr2 :=
                                 {|
                                   pr1 := Γ;
                                   pr2 :=
                                     {|
                                       pr1 := Γ';
                                       pr2 := {| pr1 := a; pr2 := p |}
                                     |}
                                 |}
                             |}
                         |})))))
    |})


DEBUG:Going to execute:
simpl

Goals:
    A : Type  P : list A → list A → A → A → Type
  ============================
   ({| pr1 := {| pr1 := []; pr2 := [] |}; pr2 := All2_fold_nil P |} =
    {| pr1 := {| pr1 := []; pr2 := [] |}; pr2 := All2_fold_nil P |})

  
  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
  ============================
   ({|
      pr1 := {| pr1 := d :: Γ; pr2 := d' :: Γ' |};
      pr2 := All2_fold_cons P a p
    |} =
    {|
      pr1 := {| pr1 := d :: Γ; pr2 := d' :: Γ' |};
      pr2 := All2_fold_cons P a p
    |})


DEBUG:Going to execute:
solve [ constructor ]
Level 5: evaluation returns
idtac of type tacvalue

Level 3: evaluation returns
idtac of type tacvalue

Level 3: evaluation returns
idtac of type tacvalue