Goal:
  
  G1 : t
  G2 : t
  on_edge : forall x y : V.t, EdgeOf G1 x y -> EdgeOf G2 x y
  weight_on_edge : forall (x y : V.t) (e : EdgeOf G1 x y),
                   (on_edge x y e).π1 <= e.π1
  s : VSet.t
  x : V.t
  y : V.t
  p : SPath G1 s x y
  s0 : VSet.t
  x0 : V.t
  y0 : V.t
  s1 : VSet.t
  y' : V.t
  d : DisjointAdd x0 s1 s0
  e : EdgeOf G1 x0 y'
  p0 : SPath G1 s1 y' y0
  H : sweight (map_spath p0) <= sweight p0
  ============================
   ((on_edge x0 y' e).π1 + sweight (map_spath p0) <= e.π1 + sweight p0)


DEBUG:Going to execute:
case not_locked_false_eq_true; Ltac.assumption
Level 1: Backtrace:

Not an inductive goal with 1 constructor.
Level 0: Backtrace:

Not an inductive goal with 1 constructor.
Level 0: Backtrace:

No applicable tactic.
Level 0: Backtrace:

No applicable tactic.