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' : VSet.t
  H4 : sigma
         (fun H : V.t =>
          sigma
            (fun H0 : V.t =>
             sigma
               (fun H1 : VSet.t =>
                sigma
                  (fun H2 : V.t =>
                   sigma
                     (fun H3 : V.t =>
                      sigma (fun _ : SPath G H4' H H0 => SPath G H1 H2 H3))))))
  H2 : SPath_direct_subterm G H4' (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))))))
         (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 |}
                        |}
                    |}
                |}
            |}
        |}
    |} = {| pr1 := H4'; pr2 := 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:
hnf in id
Level 6: evaluation returns
hnf in id;
 match type of id with
 | sigma _ =>
     let xn := fresh id "'" in
     destruct id as [xn id]; DepElim.decompose_exists xn id;
      cbv beta iota delta [TODO projection TODO projection] in id, id';
      DepElim.decompose_exists id id'
 | _ => cbv beta iota delta [TODO projection TODO projection] in id, id'
 end
where
id' := H2
of type
constr
id := H4
of type
constr of type tacvalue