Goal:
  
  G1 : t
  G2 : t
  l : labelling
  Gl := relabel_on G1 G2 l : t
  H : invariants G1
  preserves_edges : forall e : EdgeSet.elt,
                    EdgeSet.In e (E G1) -> EdgeSet.In e (E G2)
  HGl : correct_labelling G1 l
  H0 : invariants G2
  H1 : acyclic_no_loop G2
  embed : forall v1 v2 : VSet.elt,
          VSet.In v1 (V G1) ->
          VSet.In v2 (V G1) -> (lsp G2 v1 v2 <= lsp G1 v1 v2)%nbar
  G : t
  H4 : sigma
         (fun H : VSet.t =>
          sigma
            (fun H0 : V.t =>
             sigma
               (fun H1 : V.t =>
                sigma
                  (fun H2 : VSet.t =>
                   sigma
                     (fun H3 : V.t =>
                      sigma
                        (fun H4 : V.t =>
                         sigma (fun _ : SPath G H H0 H1 => SPath G H2 H3 H4)))))))
  H2 : SPath_direct_subterm G (pr1 H4) (pr1 (pr2 H4)) 
         (pr1 (pr2 (pr2 H4))) (pr1 (pr2 (pr2 (pr2 H4))))
         (pr1 (pr2 (pr2 (pr2 (pr2 H4)))))
         (pr1 (pr2 (pr2 (pr2 (pr2 (pr2 H4))))))
         (pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 H4)))))))
         (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 H4)))))))
  ============================
   (forall (s0 : VSet.t) (x : V.t) (pr1 : VSet.t) 
      (pr0 pr2 : V.t) (y0 : SPath G pr1 pr0 pr2),
    {|
      pr1 := pr1;
      pr2 :=
        {|
          pr1 := pr0;
          pr2 :=
            {|
              pr1 := pr2;
              pr2 :=
                {|
                  pr1 := s0;
                  pr2 :=
                    {|
                      pr1 := x;
                      pr2 :=
                        {|
                          pr1 := x;
                          pr2 := {| pr1 := y0; pr2 := spath_refl G s0 x |}
                        |}
                    |}
                |}
            |}
        |}
    |} = H4 ->
    let H := CoreTactics.block in
    let H0 := CoreTactics.block in
    Acc
      (fun
         x0
          y : sigma
                (fun
                   index : sigma
                             (fun _ : VSet.t => sigma (fun _ : V.t => V.t))
                 =>
                 SPath G (Init.pr1 index) (Init.pr1 (Init.pr2 index))
                   (Init.pr2 (Init.pr2 index))) =>
       SPath_direct_subterm G (Init.pr1 (Init.pr1 x0))
         (Init.pr1 (Init.pr2 (Init.pr1 x0)))
         (Init.pr2 (Init.pr2 (Init.pr1 x0))) (Init.pr1 (Init.pr1 y))
         (Init.pr1 (Init.pr2 (Init.pr1 y)))
         (Init.pr2 (Init.pr2 (Init.pr1 y))) (Init.pr2 x0) 
         (Init.pr2 y))
      {|
        pr1 := {| pr1 := pr1; pr2 := {| pr1 := pr0; pr2 := pr2 |} |};
        pr2 := y0
      |})


DEBUG:Going to execute:
rename id' into id
Level 38: evaluation returns
idtac of type tacvalue

Level 36: evaluation returns
idtac of type tacvalue

Level 35: evaluation returns
idtac of type tacvalue

Level 33: evaluation returns
idtac of type tacvalue

Level 31: evaluation returns
idtac of type tacvalue

Level 30: evaluation returns
idtac of type tacvalue

Level 28: evaluation returns
idtac of type tacvalue

Level 26: evaluation returns
idtac of type tacvalue

Level 25: evaluation returns
idtac of type tacvalue

Level 23: evaluation returns
idtac of type tacvalue

Level 21: evaluation returns
idtac of type tacvalue

Level 20: evaluation returns
idtac of type tacvalue

Level 18: evaluation returns
idtac of type tacvalue

Level 16: evaluation returns
idtac of type tacvalue

Level 15: evaluation returns
idtac of type tacvalue

Level 13: evaluation returns
idtac of type tacvalue

Level 11: evaluation returns
idtac of type tacvalue

Level 10: evaluation returns
idtac of type tacvalue

Level 8: evaluation returns
idtac of type tacvalue

Level 6: evaluation returns
idtac of type tacvalue

Level 5: evaluation returns
idtac of type tacvalue