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 s' : VSet.t) (x y z : V.t) (d : DisjointAdd x s0 s')
      (e : EdgeOf G x y) (a0 : SPath G s0 y z),
    Acc
      (fun
         x0
          y0 : sigma
                 (fun
                    index : sigma
                              (fun _ : VSet.t => sigma (fun _ : V.t => V.t))
                  => SPath G (pr1 index) (pr1 (pr2 index)) (pr2 (pr2 index)))
       =>
       SPath_direct_subterm G (pr1 (pr1 x0)) (pr1 (pr2 (pr1 x0)))
         (pr2 (pr2 (pr1 x0))) (pr1 (pr1 y0)) (pr1 (pr2 (pr1 y0)))
         (pr2 (pr2 (pr1 y0))) (pr2 x0) (pr2 y0))
      {|
        pr1 := {| pr1 := s0; pr2 := {| pr1 := y; pr2 := z |} |}; pr2 := a0
      |} ->
    forall (pr1 : VSet.t) (pr0 pr2 : V.t) (y1 : SPath G pr1 pr0 pr2),
    {|
      pr1 := pr1;
      pr2 :=
        {|
          pr1 := pr0;
          pr2 :=
            {|
              pr1 := pr2;
              pr2 :=
                {|
                  pr1 := s';
                  pr2 :=
                    {|
                      pr1 := x;
                      pr2 :=
                        {|
                          pr1 := z;
                          pr2 :=
                            {|
                              pr1 := y1;
                              pr2 := spath_step G s0 s' x y z d e a0
                            |}
                        |}
                    |}
                |}
            |}
        |}
    |} = H4 ->
    let H := CoreTactics.block in
    let H0 := CoreTactics.block in
    Acc
      (fun
         x0
          y0 : 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 y0))
         (Init.pr1 (Init.pr2 (Init.pr1 y0)))
         (Init.pr2 (Init.pr2 (Init.pr1 y0))) (Init.pr2 x0) 
         (Init.pr2 y0))
      {|
        pr1 := {| pr1 := pr1; pr2 := {| pr1 := pr0; pr2 := pr2 |} |};
        pr2 := y1
      |})


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

Level 71: evaluation returns
idtac of type tacvalue

Level 70: evaluation returns
idtac of type tacvalue

Level 68: evaluation returns
idtac of type tacvalue

Level 66: evaluation returns
idtac of type tacvalue

Level 65: evaluation returns
idtac of type tacvalue

Level 63: evaluation returns
idtac of type tacvalue

Level 61: evaluation returns
idtac of type tacvalue

Level 60: evaluation returns
idtac of type tacvalue

Level 58: evaluation returns
idtac of type tacvalue

Level 56: evaluation returns
idtac of type tacvalue

Level 55: evaluation returns
idtac of type tacvalue

Level 53: evaluation returns
idtac of type tacvalue

Level 51: evaluation returns
idtac of type tacvalue

Level 50: evaluation returns
idtac of type tacvalue

Level 48: evaluation returns
idtac of type tacvalue

Level 46: evaluation returns
idtac of type tacvalue

Level 45: evaluation returns
idtac of type tacvalue

Level 43: evaluation returns
idtac of type tacvalue

Level 41: evaluation returns
idtac of type tacvalue

Level 40: evaluation returns
idtac of type tacvalue

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