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
  s0 : VSet.t
  s' : VSet.t
  x : V.t
  y : V.t
  z : V.t
  d : DisjointAdd x s0 s'
  e : EdgeOf G x y
  p0 : SPath G s0 y z
  IHp0 : Acc
           (fun
              x
               y : 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 x)) (pr1 (pr2 (pr1 x)))
              (pr2 (pr2 (pr1 x))) (pr1 (pr1 y)) (pr1 (pr2 (pr1 y)))
              (pr2 (pr2 (pr1 y))) (pr2 x) (pr2 y))
           {|
             pr1 := {| pr1 := s0; pr2 := {| pr1 := y; pr2 := z |} |};
             pr2 := p0
           |}
  s1 : VSet.t
  x1 : V.t
  y1 : V.t
  p1 : SPath G s1 x1 y1
  h : SPath_direct_subterm G s1 x1 y1 s' x z p1
        (spath_step G s0 s' x y z d e p0)
  h0 := {|
          pr1 :=
            {|
              pr1 := s1;
              pr2 :=
                {|
                  pr1 := x1;
                  pr2 :=
                    {|
                      pr1 := y1;
                      pr2 :=
                        {|
                          pr1 := s';
                          pr2 :=
                            {|
                              pr1 := x;
                              pr2 :=
                                {|
                                  pr1 := z;
                                  pr2 :=
                                    {|
                                      pr1 := p1;
                                      pr2 := spath_step G s0 s' x y z d e p0
                                    |}
                                |}
                            |}
                        |}
                    |}
                |}
            |};
          pr2 := h
        |}
     : sigma
         (fun
            index : 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))))))) =>
          SPath_direct_subterm G (pr1 index) (pr1 (pr2 index))
            (pr1 (pr2 (pr2 index))) (pr1 (pr2 (pr2 (pr2 index))))
            (pr1 (pr2 (pr2 (pr2 (pr2 index)))))
            (pr1 (pr2 (pr2 (pr2 (pr2 (pr2 index))))))
            (pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 index)))))))
            (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 index))))))))
  h1 := {|
          pr1 := s1;
          pr2 :=
            {|
              pr1 := x1;
              pr2 :=
                {|
                  pr1 := y1;
                  pr2 :=
                    {|
                      pr1 := s';
                      pr2 :=
                        {|
                          pr1 := x;
                          pr2 :=
                            {|
                              pr1 := z;
                              pr2 :=
                                {|
                                  pr1 := p1;
                                  pr2 := spath_step G s0 s' x y z d e p0
                                |}
                            |}
                        |}
                    |}
                |}
            |}
        |}
     : 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 := h
     : (fun
          index : 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))))))) =>
        SPath_direct_subterm G (pr1 index) (pr1 (pr2 index))
          (pr1 (pr2 (pr2 index))) (pr1 (pr2 (pr2 (pr2 index))))
          (pr1 (pr2 (pr2 (pr2 (pr2 index)))))
          (pr1 (pr2 (pr2 (pr2 (pr2 (pr2 index))))))
          (pr1 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 index)))))))
          (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 (pr2 index)))))))) h1
  ============================
   (let H := CoreTactics.block in
    let H0 := CoreTactics.block in
    Acc
      (fun
         x
          y : 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 x)) (pr1 (pr2 (pr1 x)))
         (pr2 (pr2 (pr1 x))) (pr1 (pr1 y)) (pr1 (pr2 (pr1 y)))
         (pr2 (pr2 (pr1 y))) (pr2 x) (pr2 y))
      {|
        pr1 := {| pr1 := s1; pr2 := {| pr1 := x1; pr2 := y1 |} |}; pr2 := p1
      |})


DEBUG:Going to execute:
generalize (eq_refl : t = id'1)