Goal:
    G : t
  ============================
   (forall (x y : V.t) (s s' : VSet.t),
    VSet.Equal s s' -> lsp00 0 s x y = lsp00 0 s' x y)


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::reflexivity@0>