Goal:
  
  G1 : t
  G2 : t
  H : invariants G1
  H0 : invariants G2
  H1 : acyclic_no_loop G2
  hsub : subgraph G1 G2
  acG1 : acyclic_no_loop G1
  x : VSet.elt
  y : VSet.elt
  hx : VSet.In x (border_set G1 (EdgeSet.diff (E G2) (E G1)))
  hy : VSet.In y (border_set G1 (EdgeSet.diff (E G2) (E G1)))
  ============================
   ((lsp G1 x y == lsp G2 x y) = true -> (lsp G2 x y <= lsp G1 x y)%nbar)


DEBUG:Going to execute:
move  =>/(@ReflectEq.eqb_spec _ reflectEq_nbar) ->
DEBUG LTAC Evaluated term: ext
DEBUG LTAC Evaluated term: VSet.for_all_spec
DEBUG LTAC Evaluated term: (iffLR
                              (Q:=VSet.For_all
                                    (fun x : VSet.elt =>
                                     (fun x0 : VSet.elt =>
                                      VSet.for_all
                                        (fun y : VSet.elt =>
                                         lsp G1 x0 y == lsp G2 x0 y)
                                        (border_set G1
                                           (EdgeSet.diff (E G2) (E G1)))) x =
                                     true)
                                    (border_set G1
                                       (EdgeSet.diff (E G2) (E G1))))
                              (VSet.for_all_spec
                                 (border_set G1 (EdgeSet.diff (E G2) (E G1)))
                                 (f:=fun x : VSet.elt =>
                                     VSet.for_all
                                       (fun y : VSet.elt =>
                                        lsp G1 x y == lsp G2 x y)
                                       (border_set G1
                                          (EdgeSet.diff (E G2) (E G1)))) 
                                 ?p) _view_subject_)
DEBUG LTAC Evaluated term: (iffLR
                              (Q:=VSet.For_all
                                    (fun x : VSet.elt =>
                                     (fun x0 : VSet.elt =>
                                      VSet.for_all
                                        (fun y : VSet.elt =>
                                         lsp G1 x0 y == lsp G2 x0 y)
                                        (border_set G1
                                           (EdgeSet.diff (E G2) (E G1)))) x =
                                     true)
                                    (border_set G1
                                       (EdgeSet.diff (E G2) (E G1))))
                              (VSet.for_all_spec
                                 (border_set G1 (EdgeSet.diff (E G2) (E G1)))
                                 (f:=fun x : VSet.elt =>
                                     VSet.for_all
                                       (fun y : VSet.elt =>
                                        lsp G1 x y == lsp G2 x y)
                                       (border_set G1
                                          (EdgeSet.diff (E G2) (E G1)))) 
                                 ?p) _view_subject_ x hx)
DEBUG LTAC Evaluated term: VSet.for_all_spec
DEBUG LTAC Evaluated term: (iffLR
                              (Q:=VSet.For_all
                                    (fun x0 : VSet.elt =>
                                     (fun y : VSet.elt =>
                                      lsp G1 x y == lsp G2 x y) x0 = true)
                                    (border_set G1
                                       (EdgeSet.diff (E G2) (E G1))))
                              (VSet.for_all_spec
                                 (border_set G1 (EdgeSet.diff (E G2) (E G1)))
                                 (f:=fun y : VSet.elt =>
                                     lsp G1 x y == lsp G2 x y) 
                                 ?p0)
                              (iffLR
                                 (Q:=VSet.For_all
                                       (fun x : VSet.elt =>
                                        (fun x0 : VSet.elt =>
                                         VSet.for_all
                                           (fun y : VSet.elt =>
                                            lsp G1 x0 y == lsp G2 x0 y)
                                           (border_set G1
                                              (EdgeSet.diff (E G2) (E G1))))
                                          x = true)
                                       (border_set G1
                                          (EdgeSet.diff (E G2) (E G1))))
                                 (VSet.for_all_spec
                                    (border_set G1
                                       (EdgeSet.diff (E G2) (E G1)))
                                    (f:=fun x : VSet.elt =>
                                        VSet.for_all
                                          (fun y : VSet.elt =>
                                           lsp G1 x y == lsp G2 x y)
                                          (border_set G1
                                             (EdgeSet.diff (E G2) (E G1))))
                                    ?p) _view_subject_ x hx))
DEBUG LTAC Evaluated term: (iffLR
                              (Q:=VSet.For_all
                                    (fun x0 : VSet.elt =>
                                     (fun y : VSet.elt =>
                                      lsp G1 x y == lsp G2 x y) x0 = true)
                                    (border_set G1
                                       (EdgeSet.diff (E G2) (E G1))))
                              (VSet.for_all_spec
                                 (border_set G1 (EdgeSet.diff (E G2) (E G1)))
                                 (f:=fun y : VSet.elt =>
                                     lsp G1 x y == lsp G2 x y) 
                                 ?p0)
                              (iffLR
                                 (Q:=VSet.For_all
                                       (fun x : VSet.elt =>
                                        (fun x0 : VSet.elt =>
                                         VSet.for_all
                                           (fun y : VSet.elt =>
                                            lsp G1 x0 y == lsp G2 x0 y)
                                           (border_set G1
                                              (EdgeSet.diff (E G2) (E G1))))
                                          x = true)
                                       (border_set G1
                                          (EdgeSet.diff (E G2) (E G1))))
                                 (VSet.for_all_spec
                                    (border_set G1
                                       (EdgeSet.diff (E G2) (E G1)))
                                    (f:=fun x : VSet.elt =>
                                        VSet.for_all
                                          (fun y : VSet.elt =>
                                           lsp G1 x y == lsp G2 x y)
                                          (border_set G1
                                             (EdgeSet.diff (E G2) (E G1))))
                                    ?p) _view_subject_ x hx) y hy)